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

Theorem con2d 614
 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 605 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 78 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 606 . 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 604  ax-in2 605 This theorem is referenced by:  mt2d  615  con3d  621  pm3.2im  627  con2  633  pm2.65  649  con1biimdc  859  exists2  2103  necon2ad  2384  necon2bd  2385  minel  3455  nlimsucg  4523  poirr2  4975  funun  5211  imadif  5247  infnlbti  6962  mkvprop  7084  addnidpig  7239  zltnle  9196  zdcle  9223  btwnnz  9241  prime  9246  icc0r  9812  fznlem  9925  qltnle  10127  bcval4  10608  seq3coll  10695  fsum3cvg  11257  fsumsplit  11286  fproddccvg  11451  fprodsplitdc  11475  2sqpwodd  12030  logbgcd1irr  13244
 Copyright terms: Public domain W3C validator