ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con2d GIF version

Theorem con2d 598
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
Hypothesis
Ref Expression
con2d.1 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
con2d (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d
StepHypRef Expression
1 con2d.1 . . . 4 (𝜑 → (𝜓 → ¬ 𝜒))
2 ax-in2 589 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 78 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 590 . 2 ((𝜓 → ¬ 𝜓) → ¬ 𝜓)
64, 5syl6 33 1 (𝜑 → (𝜒 → ¬ 𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 588  ax-in2 589
This theorem is referenced by:  mt2d  599  con3d  605  pm3.2im  611  con2  617  pm2.65  633  con1biimdc  843  exists2  2074  necon2ad  2342  necon2bd  2343  minel  3394  nlimsucg  4451  poirr2  4901  funun  5137  imadif  5173  infnlbti  6881  mkvprop  7000  addnidpig  7112  zltnle  9068  zdcle  9095  btwnnz  9113  prime  9118  icc0r  9677  fznlem  9789  qltnle  9991  bcval4  10466  seq3coll  10553  fsum3cvg  11114  fsumsplit  11144  2sqpwodd  11781
  Copyright terms: Public domain W3C validator