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

Theorem con2d 109
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 106 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 30 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 99 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2  110  mt2d  111  pm3.2im  139  exists2  2344  necon3ad  2603  necon2bd  2616  necon4ad  2628  spcimegf  2990  spcegf  2992  spcimedv  2995  rspcimedv  3014  minel  3643  disjxun  4170  sotric  4489  sotrieq  4490  onnminsb  4743  oneqmin  4744  ordunisuc2  4783  limsssuc  4789  poirr2  5217  funun  5454  imadif  5487  soisoi  6007  tz7.48lem  6657  sdomdif  7214  pssinf  7278  unblem1  7318  supnub  7423  elirrv  7521  inf3lem6  7544  cantnflem1  7601  cardne  7808  cardsdomel  7817  carddom2  7820  cardmin2  7841  alephnbtwn  7908  infdif2  8046  fin4en1  8145  fin23lem31  8179  isf32lem5  8193  isf34lem4  8213  cfpwsdom  8415  fpwwe2  8474  addnidpi  8734  genpnnp  8838  btwnnz  10302  prime  10306  qsqueeze  10743  xralrple  10747  xmullem2  10800  xmulneg1  10804  elfznelfzob  11148  bcval4  11553  hashtpg  11646  seqcoll  11667  fsumcvg  12461  fsumsplit  12488  dvdsle  12850  divalglem8  12875  bitsinv1lem  12908  pockthg  13229  prmunb  13237  vdwlem6  13309  ramlb  13342  gsumzsplit  15484  opsrtoslem2  16500  obselocv  16910  elcls  17092  fbasrn  17869  ufilb  17891  ufilmax  17892  rnelfmlem  17937  alexsubALTlem4  18034  tsmssplit  18134  recld2  18798  fsumharmonic  20803  chtub  20949  lgsne0  21070  nbusgra  21393  nbgranself  21399  usgrasscusgra  21445  cyclnspth  21571  eupath2lem3  21654  cvnsym  23746  cvntr  23748  atcvati  23842  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemfrcn0  24740  ballotlemirc  24742  fprodcvg  25209  fprodsplit  25242  dfpo2  25326  wfrlem10  25479  sltres  25532  nodenselem5  25553  nocvxminlem  25558  nobndup  25568  nobnddown  25569  nofulllem5  25574  axlowdim  25804  onsucconi  26091  onint1  26103  nn0prpw  26216  fdc  26339  rencldnfilem  26771  stoweidlem34  27650  swrdnd  28001  lsatcvat  29533  hlrelat2  29885  ltltncvr  29905  islln2a  29999  islpln2a  30030  islvol2aN  30074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator