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  2373  necon3adOLD  2652  necon2bd  2656  necon4adOLD  2662  spcimegf  3172  spcegf  3174  spcimedv  3177  rspcimedv  3196  minel  3864  disjxun  4431  sotric  4812  sotrieq  4813  poirr2  5377  funun  5616  imadif  5649  soisoi  6205  onnminsb  6620  oneqmin  6621  ordunisuc2  6660  limsssuc  6666  tz7.48lem  7104  sdomdif  7663  pssinf  7728  unblem1  7770  supnub  7920  elirrv  8021  inf3lem6  8048  cantnflem1  8106  cantnflem1OLD  8129  cardne  8344  cardsdomel  8353  carddom2  8356  cardmin2  8377  alephnbtwn  8450  infdif2  8588  fin4en1  8687  fin23lem31  8721  isf32lem5  8735  isf34lem4  8755  cfpwsdom  8957  fpwwe2  9019  addnidpi  9277  genpnnp  9381  btwnnz  10940  prime  10944  qsqueeze  11404  xralrple  11408  xmullem2  11461  xmulneg1  11465  ssfzoulel  11880  elfznelfzob  11890  bcval4  12359  seqcoll  12486  hashtpg  12497  swrdnd  12631  swrd0  12632  fsumcvg  13508  fsumsplit  13536  dvdsle  13903  divalglem8  13930  bitsinv1lem  13963  pockthg  14296  prmunb  14304  vdwlem6  14376  ramlb  14409  gsumzsplit  16813  gsumzsplitOLD  16814  opsrtoslem2  18017  obselocv  18626  elcls  19440  fbasrn  20251  ufilb  20273  ufilmax  20274  rnelfmlem  20319  alexsubALTlem4  20416  tsmssplit  20520  recld2  21185  fsumharmonic  23206  chtub  23352  lgsne0  23473  axlowdim  24129  nbusgra  24293  nbgranself  24299  usgrasscusgra  24348  cyclnspth  24496  eupath2lem3  24844  cvnsym  27074  cvntr  27076  atcvati  27170  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemfrcn0  28334  ballotlemirc  28336  fprodcvg  29030  fprodsplit  29063  dfpo2  29152  wfrlem10  29320  sltres  29392  nodenselem5  29413  nocvxminlem  29418  nobndup  29428  nobnddown  29429  nofulllem5  29434  onsucconi  29870  onint1  29882  nn0prpw  30109  fdc  30206  rencldnfilem  30722  radcnvrat  31164  stoweidlem34  31701  lsatcvat  34477  hlrelat2  34829  ltltncvr  34849  islln2a  34943  islpln2a  34974  islvol2aN  35018
  Copyright terms: Public domain W3C validator