Theorem pm2.61d 127

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 11	. 2 ⊢ (ψ → (φ → χ))
3		pm2.61d.2	. . 3 ⊢ (φ → (¬ ψ → χ))
4	3	com12 11	. 2 ⊢ (¬ ψ → (φ → χ))
5	2, 4	pm2.61i 126	1 ⊢ (φ → χ)

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.61d1 128  pm2.61d2 129  pm2.61dan 477  a12stdy4 1374  pm2.61dne 1633  ordsson 2987  ordunidif 3001  findsg 3153  tfindsg 3158  fvco 3769  dff2 3812  omwordi 4195  omass 4204  eceqopreq 4306  pssnn 4522  unxpdomlem 4826  prlem936 5138  ssgt0sr 5200  suppsr2 5206  suppsr3 5207  elcncf 7217  cnconst 7740  atdmd 10281  atmd2 10283  mdsymlem4 10289

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

Copyright terms: Public domain