MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2d Structured version   Unicode version

Theorem con2d 115
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1  |-  ( ph  ->  ( ps  ->  -.  ch ) )
Assertion
Ref Expression
con2d  |-  ( ph  ->  ( ch  ->  -.  ps ) )

Proof of Theorem con2d
StepHypRef Expression
1 notnot2 112 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 32 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 105 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  con2  116  mt2d  117  pm3.2im  145  exists2  2377  necon3ad  2649  necon2bd  2665  necon4ad  2677  spcimegf  3056  spcegf  3058  spcimedv  3061  rspcimedv  3080  minel  3739  disjxun  4295  sotric  4672  sotrieq  4673  poirr2  5227  funun  5465  imadif  5498  soisoi  6024  onnminsb  6420  oneqmin  6421  ordunisuc2  6460  limsssuc  6466  tz7.48lem  6901  sdomdif  7464  pssinf  7528  unblem1  7569  supnub  7717  elirrv  7817  inf3lem6  7844  cantnflem1  7902  cantnflem1OLD  7925  cardne  8140  cardsdomel  8149  carddom2  8152  cardmin2  8173  alephnbtwn  8246  infdif2  8384  fin4en1  8483  fin23lem31  8517  isf32lem5  8531  isf34lem4  8551  cfpwsdom  8753  fpwwe2  8815  addnidpi  9075  genpnnp  9179  btwnnz  10723  prime  10727  qsqueeze  11176  xralrple  11180  xmullem2  11233  xmulneg1  11237  ssfzoulel  11626  elfznelfzob  11636  bcval4  12088  hashtpg  12191  seqcoll  12221  swrdnd  12331  swrd0  12332  fsumcvg  13194  fsumsplit  13221  dvdsle  13583  divalglem8  13609  bitsinv1lem  13642  pockthg  13972  prmunb  13980  vdwlem6  14052  ramlb  14085  gsumzsplit  16423  gsumzsplitOLD  16424  opsrtoslem2  17571  obselocv  18158  elcls  18682  fbasrn  19462  ufilb  19484  ufilmax  19485  rnelfmlem  19530  alexsubALTlem4  19627  tsmssplit  19731  recld2  20396  fsumharmonic  22410  chtub  22556  lgsne0  22677  axlowdim  23212  nbusgra  23344  nbgranself  23350  usgrasscusgra  23396  cyclnspth  23522  eupath2lem3  23605  cvnsym  25699  cvntr  25701  atcvati  25795  ballotlemfc0  26880  ballotlemfcc  26881  ballotlemfrcn0  26917  ballotlemirc  26919  fprodcvg  27448  fprodsplit  27481  dfpo2  27570  wfrlem10  27738  sltres  27810  nodenselem5  27831  nocvxminlem  27836  nobndup  27846  nobnddown  27847  nofulllem5  27852  onsucconi  28288  onint1  28300  nn0prpw  28523  fdc  28646  rencldnfilem  29164  stoweidlem34  29834  lsatcvat  32700  hlrelat2  33052  ltltncvr  33072  islln2a  33166  islpln2a  33197  islvol2aN  33241
  Copyright terms: Public domain W3C validator