ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con2d Structured version   Unicode 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  560  pm3.2im  565  con2  571  pm2.65  584  con1biimdc  766  exists2  1994  necon2ad  2256  necon2bd  2257  minel  3277  nlimsucg  4242  poirr2  4660  funun  4887  imadif  4922  addnidpig  6320  zltnle  8027  zdcle  8053  btwnnz  8070  prime  8073  icc0r  8525  fznlem  8635
  Copyright terms: Public domain W3C validator