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

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

Proof of Theorem con3d
StepHypRef Expression
1 notnot2 104 . . 3 (¬ ¬ ψψ)
2 con3d.1 . . 3 (φ → (ψχ))
31, 2syl5 28 . 2 (φ → (¬ ¬ ψχ))
43con1d 116 1 (φ → (¬ χ → ¬ ψ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem is referenced by:  con3  126  con3rr3  128  nsyld  132  nsyli  133  mth8  138  pm2.52  147  pm5.21ndd  343  bija  344  con3and  428  ax12bOLD  1690  ax12olem1  1927  spime  1976  mo  2226  necon1bd  2584  rexim  2718  spcimegf  2933  spcimedv  2938  rspcimedv  2957  ssneld  3275  sscon  3400  difrab  3529  ssofss  4076  pwadjoin  4119  nnsucelrlem2  4425  nnadjoin  4520  sfinltfin  4535  vfinspsslem1  4550  phi11lem1  4595  phialllem1  4616  eqfnfv  5392  dff3  5420  ndmovg  5613  nchoicelem3  6291
  Copyright terms: Public domain W3C validator