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

Theorem con2d 119
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 116 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 34 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 109 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  120  mt2d  121  pm3.2im  149  exists2  2362  necon3adOLD  2636  necon2bd  2640  necon4adOLD  2646  spcimegf  3166  spcegf  3168  spcimedv  3171  rspcimedv  3190  minel  3856  disjxun  4427  sotric  4806  sotrieq  4807  poirr2  5249  funun  5649  imadif  5682  soisoi  6240  onnminsb  6651  oneqmin  6652  ordunisuc2  6691  limsssuc  6697  wfrlem10  7062  tz7.48lem  7175  sdomdif  7735  pssinf  7797  unblem1  7838  supnub  7991  infnlb  8023  elirrv  8127  inf3lem6  8153  cantnflem1  8208  cardne  8413  cardsdomel  8422  carddom2  8425  cardmin2  8446  alephnbtwn  8515  infdif2  8653  fin4en1  8752  fin23lem31  8786  isf32lem5  8800  isf34lem4  8820  cfpwsdom  9022  fpwwe2  9081  addnidpi  9339  genpnnp  9443  btwnnz  11025  prime  11029  qsqueeze  11507  xralrple  11511  xmullem2  11564  xmulneg1  11568  ssfzoulel  12017  elfznelfzob  12027  bcval4  12504  seqcoll  12637  hashtpg  12651  swrd0  12798  fsumcvg  13783  fsumsplit  13811  fprodcvg  13989  fprodsplit  14025  dvdsle  14355  divalglem8  14385  bitsinv1lem  14420  pockthg  14855  prmunb  14863  vdwlem6  14941  ramlb  14982  gsumzsplit  17565  opsrtoslem2  18713  obselocv  19295  elcls  20093  fbasrn  20903  ufilb  20925  ufilmax  20926  rnelfmlem  20971  alexsubALTlem4  21069  tsmssplit  21170  recld2  21836  fsumharmonic  23941  chtub  24144  lgsne0  24265  axlowdim  24995  nbusgra  25160  nbgranself  25166  usgrasscusgra  25215  cyclnspth  25363  eupath2lem3  25711  cvnsym  27947  cvntr  27949  atcvati  28043  ballotlemfc0  29339  ballotlemfcc  29340  ballotlemfrcn0  29376  ballotlemirc  29378  ballotlemfrcn0OLD  29414  ballotlemircOLD  29416  dfpo2  30408  sltres  30564  nodenselem5  30585  nocvxminlem  30590  nobndup  30600  nobnddown  30601  nofulllem5  30606  nn0prpw  30990  onsucconi  31108  onint1  31120  icorempt2  31724  relowlpssretop  31737  poimirlem16  31926  poimirlem26  31936  fdc  32044  lsatcvat  32591  hlrelat2  32943  ltltncvr  32963  islln2a  33057  islpln2a  33088  islvol2aN  33132  rencldnfilem  35638  ss2iundf  36227  radcnvrat  36639  stoweidlem34  37841  oddneven  38650  nbgrssovtx  39194
  Copyright terms: Public domain W3C validator