MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2d Structured version   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  2371  necon3ad  2637  necon2bd  2653  necon4ad  2665  spcimegf  3030  spcegf  3032  spcimedv  3035  rspcimedv  3054  minel  3683  disjxun  4210  sotric  4529  sotrieq  4530  onnminsb  4784  oneqmin  4785  ordunisuc2  4824  limsssuc  4830  poirr2  5258  funun  5495  imadif  5528  soisoi  6048  tz7.48lem  6698  sdomdif  7255  pssinf  7319  unblem1  7359  supnub  7467  elirrv  7565  inf3lem6  7588  cantnflem1  7645  cardne  7852  cardsdomel  7861  carddom2  7864  cardmin2  7885  alephnbtwn  7952  infdif2  8090  fin4en1  8189  fin23lem31  8223  isf32lem5  8237  isf34lem4  8257  cfpwsdom  8459  fpwwe2  8518  addnidpi  8778  genpnnp  8882  btwnnz  10346  prime  10350  qsqueeze  10787  xralrple  10791  xmullem2  10844  xmulneg1  10848  elfznelfzob  11193  bcval4  11598  hashtpg  11691  seqcoll  11712  fsumcvg  12506  fsumsplit  12533  dvdsle  12895  divalglem8  12920  bitsinv1lem  12953  pockthg  13274  prmunb  13282  vdwlem6  13354  ramlb  13387  gsumzsplit  15529  opsrtoslem2  16545  obselocv  16955  elcls  17137  fbasrn  17916  ufilb  17938  ufilmax  17939  rnelfmlem  17984  alexsubALTlem4  18081  tsmssplit  18181  recld2  18845  fsumharmonic  20850  chtub  20996  lgsne0  21117  nbusgra  21440  nbgranself  21446  usgrasscusgra  21492  cyclnspth  21618  eupath2lem3  21701  cvnsym  23793  cvntr  23795  atcvati  23889  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemfrcn0  24787  ballotlemirc  24789  fprodcvg  25256  fprodsplit  25289  dfpo2  25378  wfrlem10  25547  sltres  25619  nodenselem5  25640  nocvxminlem  25645  nobndup  25655  nobnddown  25656  nofulllem5  25661  axlowdim  25900  onsucconi  26187  onint1  26199  nn0prpw  26326  fdc  26449  rencldnfilem  26881  stoweidlem34  27759  swrdnd  28182  swrdvalodmlem1  28187  lsatcvat  29848  hlrelat2  30200  ltltncvr  30220  islln2a  30314  islpln2a  30345  islvol2aN  30389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator