Theorem pm2.61d 112

Description: Deduction eliminating an antecedent.

Hypotheses

Ref	Expression
pm2.61d.1	⊢ (φ → (ψ → χ))
pm2.61d.2	⊢ (φ → (¬ ψ → χ))

Assertion

Ref	Expression
pm2.61d	⊢ (φ → χ)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	com12 13	. 2 ⊢ (ψ → (φ → χ))
3		pm2.61d.2	. . 3 ⊢ (φ → (¬ ψ → χ))
4	3	com12 13	. 2 ⊢ (¬ ψ → (φ → χ))
5	2, 4	pm2.61i 110	1 ⊢ (φ → χ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.61an2 365  wefrc 2195  ordsson 2242  ordunidif 2260  findsg 2398  tfindsg 2402  funfv 2862  fvco 2865  oe0lem 3121  eceqopreq 3249  pssnn 3428  unxpdomlem 3649  alephon 3671  prlem936 3949  ssgt0sr 4011  suppsr2 4017  suppsr3 4018  uzwo 4605  mdsymlem4 5779

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org