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

Theorem con3d 621
 Description: A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
Hypothesis
Ref Expression
con3d.1
Assertion
Ref Expression
con3d

Proof of Theorem con3d
StepHypRef Expression
1 con3d.1 . . 3
2 notnot 619 . . 3
31, 2syl6 33 . 2
43con2d 614 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:  con3rr3  623  con3dimp  625  con3  632  nsyld  638  nsyli  639  jcn  641  notbi  656  impidc  844  bijadc  868  pm2.13dc  871  xoranor  1356  mo2n  2028  necon3ad  2351  necon3bd  2352  nelcon3d  2415  ssneld  3105  sscon  3216  difrab  3356  eunex  4485  ndmfvg  5461  nnaord  6414  nnmord  6422  php5  6761  php5dom  6766  supmoti  6890  exmidomniim  7023  mkvprop  7042  enmkvlem  7045  prubl  7338  letr  7891  eqord1  8289  cnstab  8451  prodge0  8656  lt2msq  8688  nnge1  8787  nzadd  9150  irradd  9485  irrmul  9486  xrletr  9641  frec2uzf1od  10230  zesq  10461  expcanlem  10513  nn0opthd  10520  bccmpl  10552  maxleast  11037  fisumss  11213  dvdsbnd  11701  prm2orodd  11863  coprm  11878  prmndvdsfaclt  11890  hashgcdeq  11960  cos11  13002  bj-nnsn  13136  bj-nnelirr  13342  exmid1stab  13387  ismkvnnlem  13441  nconstwlpolem  13453
 Copyright terms: Public domain W3C validator