NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  con2d GIF version

Theorem con2d 107
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1 (φ → (ψ → ¬ χ))
Assertion
Ref Expression
con2d (φ → (χ → ¬ ψ))

Proof of Theorem con2d
StepHypRef Expression
1 notnot2 104 . . 3 (¬ ¬ ψψ)
2 con2d.1 . . 3 (φ → (ψ → ¬ χ))
31, 2syl5 28 . 2 (φ → (¬ ¬ ψ → ¬ χ))
43con4d 97 1 (φ → (χ → ¬ ψ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con2  108  mt2d  109  pm3.2im  137  exists2  2294  necon3ad  2552  necon2bd  2565  necon4ad  2577  spcimegf  2933  spcegf  2935  spcimedv  2938  rspcimedv  2957  minel  3606  tfinltfin  4501  tfinnn  4534  imadif  5171  nchoicelem14  6302
  Copyright terms: Public domain W3C validator