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

Theorem con4d 97
Description: Deduction derived from Axiom ax-3 8. (Contributed by NM, 26-Mar-1995.)
Hypothesis
Ref Expression
con4d.1 (φ → (¬ ψ → ¬ χ))
Assertion
Ref Expression
con4d (φ → (χψ))

Proof of Theorem con4d
StepHypRef Expression
1 con4d.1 . 2 (φ → (¬ ψ → ¬ χ))
2 ax-3 8 . 2 ((¬ ψ → ¬ χ) → (χψ))
31, 2syl 15 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:  pm2.21d  98  pm2.18  102  con2d  107  con1d  116  mt4d  130  impcon4bid  196  con4bid  284  exim  1575  sp  1747  spOLD  1748  axi11e  2332  necon2ad  2564  spc2gv  2942  spc3gv  2944  addceq0  6219
  Copyright terms: Public domain W3C validator