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

Theorem con2d 624
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 615 . . . 4 𝜒 → (𝜒 → ¬ 𝜓))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒 → ¬ 𝜓)))
43com23 78 . 2 (𝜑 → (𝜒 → (𝜓 → ¬ 𝜓)))
5 pm2.01 616 . 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 614  ax-in2 615
This theorem is referenced by:  mt2d  625  con3d  631  pm3.2im  637  con2  643  pm2.65  659  con1biimdc  873  exists2  2123  necon2ad  2404  necon2bd  2405  minel  3484  nlimsucg  4565  poirr2  5021  funun  5260  imadif  5296  infnlbti  7024  mkvprop  7155  addnidpig  7334  zltnle  9297  zdcle  9327  btwnnz  9345  prime  9350  icc0r  9924  fznlem  10038  qltnle  10243  bcval4  10727  seq3coll  10817  fsum3cvg  11381  fsumsplit  11410  fproddccvg  11575  fprodsplitdc  11599  2sqpwodd  12170  pockthg  12349  prmunb  12354  logbgcd1irr  14278  lgsne0  14332
  Copyright terms: Public domain W3C validator