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

Theorem con2d 587
 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 578 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 77 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 579 . 2 ((𝜓 → ¬ 𝜓) → ¬ 𝜓)
64, 5syl6 33 1 (𝜑 → (𝜒 → ¬ 𝜓))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578 This theorem is referenced by:  mt2d  588  con3d  594  pm3.2im  599  con2  605  pm2.65  618  con1biimdc  801  exists2  2039  necon2ad  2303  necon2bd  2304  minel  3312  nlimsucg  4317  poirr2  4747  funun  4974  imadif  5010  infnlbti  6498  addnidpig  6588  zltnle  8478  zdcle  8505  btwnnz  8522  prime  8527  icc0r  9025  fznlem  9136  qltnle  9332  bcval4  9776  fisumcvg  10338  2sqpwodd  10698
 Copyright terms: Public domain W3C validator