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

Theorem con2d 596
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 587 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 78 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 588 . 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 586  ax-in2 587
This theorem is referenced by:  mt2d  597  con3d  603  pm3.2im  609  con2  615  pm2.65  631  con1biimdc  841  exists2  2072  necon2ad  2340  necon2bd  2341  minel  3392  nlimsucg  4449  poirr2  4899  funun  5135  imadif  5171  infnlbti  6879  mkvprop  6998  addnidpig  7108  zltnle  9054  zdcle  9081  btwnnz  9099  prime  9104  icc0r  9660  fznlem  9772  qltnle  9974  bcval4  10449  seq3coll  10536  fsum3cvg  11097  fsumsplit  11127  2sqpwodd  11760
  Copyright terms: Public domain W3C validator