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

Theorem con2d 554
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 545 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 29 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 72 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 546 . 2 ((𝜓 → ¬ 𝜓) → ¬ 𝜓)
64, 5syl6 29 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 544  ax-in2 545
This theorem is referenced by:  mt2d  555  con3d  561  pm3.2im  566  con2  572  pm2.65  585  con1biimdc  767  exists2  1997  necon2ad  2259  necon2bd  2260  minel  3280  nlimsucg  4284  poirr2  4704  funun  4931  imadif  4966  addnidpig  6415  zltnle  8263  zdcle  8289  btwnnz  8306  prime  8309  icc0r  8762  fznlem  8872
  Copyright terms: Public domain W3C validator