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  2262  necon2bd  2263  minel  3283  nlimsucg  4290  poirr2  4717  funun  4944  imadif  4979  addnidpig  6434  zltnle  8291  zdcle  8317  btwnnz  8334  prime  8337  icc0r  8795  fznlem  8905  qltnle  9101
  Copyright terms: Public domain W3C validator