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  2399  necon3adOLD  2678  necon2bd  2682  necon4adOLD  2688  spcimegf  3192  spcegf  3194  spcimedv  3197  rspcimedv  3216  minel  3882  disjxun  4445  sotric  4826  sotrieq  4827  poirr2  5389  funun  5628  imadif  5661  soisoi  6210  onnminsb  6617  oneqmin  6618  ordunisuc2  6657  limsssuc  6663  tz7.48lem  7103  sdomdif  7662  pssinf  7727  unblem1  7768  supnub  7918  elirrv  8019  inf3lem6  8046  cantnflem1  8104  cantnflem1OLD  8127  cardne  8342  cardsdomel  8351  carddom2  8354  cardmin2  8375  alephnbtwn  8448  infdif2  8586  fin4en1  8685  fin23lem31  8719  isf32lem5  8733  isf34lem4  8753  cfpwsdom  8955  fpwwe2  9017  addnidpi  9275  genpnnp  9379  btwnnz  10933  prime  10937  qsqueeze  11396  xralrple  11400  xmullem2  11453  xmulneg1  11457  ssfzoulel  11870  elfznelfzob  11880  bcval4  12349  seqcoll  12474  hashtpg  12485  swrdnd  12616  swrd0  12617  fsumcvg  13493  fsumsplit  13521  dvdsle  13886  divalglem8  13913  bitsinv1lem  13946  pockthg  14279  prmunb  14287  vdwlem6  14359  ramlb  14392  gsumzsplit  16735  gsumzsplitOLD  16736  opsrtoslem2  17920  obselocv  18526  elcls  19340  fbasrn  20120  ufilb  20142  ufilmax  20143  rnelfmlem  20188  alexsubALTlem4  20285  tsmssplit  20389  recld2  21054  fsumharmonic  23069  chtub  23215  lgsne0  23336  axlowdim  23940  nbusgra  24104  nbgranself  24110  usgrasscusgra  24159  cyclnspth  24307  eupath2lem3  24655  cvnsym  26885  cvntr  26887  atcvati  26981  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemfrcn0  28108  ballotlemirc  28110  fprodcvg  28639  fprodsplit  28672  dfpo2  28761  wfrlem10  28929  sltres  29001  nodenselem5  29022  nocvxminlem  29027  nobndup  29037  nobnddown  29038  nofulllem5  29043  onsucconi  29479  onint1  29491  nn0prpw  29718  fdc  29841  rencldnfilem  30358  stoweidlem34  31334  lsatcvat  33847  hlrelat2  34199  ltltncvr  34219  islln2a  34313  islpln2a  34344  islvol2aN  34388
  Copyright terms: Public domain W3C validator