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  2368  necon3ad  2634  necon2bd  2650  necon4ad  2662  spcimegf  3040  spcegf  3042  spcimedv  3045  rspcimedv  3064  minel  3722  disjxun  4278  sotric  4654  sotrieq  4655  poirr2  5210  funun  5448  imadif  5481  soisoi  6006  onnminsb  6404  oneqmin  6405  ordunisuc2  6444  limsssuc  6450  tz7.48lem  6882  sdomdif  7447  pssinf  7511  unblem1  7552  supnub  7700  elirrv  7800  inf3lem6  7827  cantnflem1  7885  cantnflem1OLD  7908  cardne  8123  cardsdomel  8132  carddom2  8135  cardmin2  8156  alephnbtwn  8229  infdif2  8367  fin4en1  8466  fin23lem31  8500  isf32lem5  8514  isf34lem4  8534  cfpwsdom  8736  fpwwe2  8797  addnidpi  9057  genpnnp  9161  btwnnz  10705  prime  10709  qsqueeze  11158  xralrple  11162  xmullem2  11215  xmulneg1  11219  ssfzoulel  11604  elfznelfzob  11614  bcval4  12066  hashtpg  12169  seqcoll  12199  swrdnd  12309  swrd0  12310  fsumcvg  13172  fsumsplit  13199  dvdsle  13560  divalglem8  13586  bitsinv1lem  13619  pockthg  13949  prmunb  13957  vdwlem6  14029  ramlb  14062  gsumzsplit  16397  gsumzsplitOLD  16398  opsrtoslem2  17497  obselocv  17994  elcls  18518  fbasrn  19298  ufilb  19320  ufilmax  19321  rnelfmlem  19366  alexsubALTlem4  19463  tsmssplit  19567  recld2  20232  fsumharmonic  22289  chtub  22435  lgsne0  22556  axlowdim  23029  nbusgra  23161  nbgranself  23167  usgrasscusgra  23213  cyclnspth  23339  eupath2lem3  23422  cvnsym  25516  cvntr  25518  atcvati  25612  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemfrcn0  26759  ballotlemirc  26761  fprodcvg  27289  fprodsplit  27322  dfpo2  27411  wfrlem10  27579  sltres  27651  nodenselem5  27672  nocvxminlem  27677  nobndup  27687  nobnddown  27688  nofulllem5  27693  onsucconi  28130  onint1  28142  nn0prpw  28359  fdc  28482  rencldnfilem  29001  stoweidlem34  29672  lsatcvat  32265  hlrelat2  32617  ltltncvr  32637  islln2a  32731  islpln2a  32762  islvol2aN  32806
  Copyright terms: Public domain W3C validator