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

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

Proof of Theorem con1d
StepHypRef Expression
1 con1d.1 . . 3 (φ → (¬ ψχ))
2 notnot1 114 . . 3 (χ → ¬ ¬ χ)
31, 2syl6 29 . 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:  mt3d  117  con1  120  con3d  125  pm2.24d  135  pm2.61d  150  pm2.8  823  dedlem0b  919  meredith  1404  19.9ht  1778  19.9tOLD  1857  ax12olem3  1929  necon3bd  2553  necon4bd  2578  necon1ad  2583  sspss  3368  neldif  3391  nnsucelr  4428  funiunfv  5467
  Copyright terms: Public domain W3C validator