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

Theorem con2d 118
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 115 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 33 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 108 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  119  mt2d  120  pm3.2im  148  exists2  2367  necon3adOLD  2642  necon2bd  2646  necon4adOLD  2652  spcimegf  3166  spcegf  3168  spcimedv  3171  rspcimedv  3190  minel  3854  disjxun  4424  sotric  4801  sotrieq  4802  poirr2  5244  funun  5643  imadif  5676  soisoi  6234  onnminsb  6645  oneqmin  6646  ordunisuc2  6685  limsssuc  6691  wfrlem10  7053  tz7.48lem  7166  sdomdif  7726  pssinf  7788  unblem1  7829  supnub  7982  infnlb  8014  elirrv  8112  inf3lem6  8138  cantnflem1  8193  cardne  8398  cardsdomel  8407  carddom2  8410  cardmin2  8431  alephnbtwn  8500  infdif2  8638  fin4en1  8737  fin23lem31  8771  isf32lem5  8785  isf34lem4  8805  cfpwsdom  9007  fpwwe2  9067  addnidpi  9325  genpnnp  9429  btwnnz  11012  prime  11016  qsqueeze  11494  xralrple  11498  xmullem2  11551  xmulneg1  11555  ssfzoulel  12002  elfznelfzob  12012  bcval4  12489  seqcoll  12621  hashtpg  12632  swrd0  12775  fsumcvg  13756  fsumsplit  13784  fprodcvg  13962  fprodsplit  13998  dvdsle  14328  divalglem8  14356  bitsinv1lem  14389  pockthg  14813  prmunb  14821  vdwlem6  14899  ramlb  14940  gsumzsplit  17495  opsrtoslem2  18643  obselocv  19222  elcls  20020  fbasrn  20830  ufilb  20852  ufilmax  20853  rnelfmlem  20898  alexsubALTlem4  20996  tsmssplit  21097  recld2  21743  fsumharmonic  23802  chtub  24003  lgsne0  24124  axlowdim  24837  nbusgra  25001  nbgranself  25007  usgrasscusgra  25056  cyclnspth  25204  eupath2lem3  25552  cvnsym  27778  cvntr  27780  atcvati  27874  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemfrcn0  29188  ballotlemirc  29190  dfpo2  30182  sltres  30338  nodenselem5  30359  nocvxminlem  30364  nobndup  30374  nobnddown  30375  nofulllem5  30380  nn0prpw  30764  onsucconi  30882  onint1  30894  icorempt2  31488  relowlpssretop  31501  poimirlem16  31660  poimirlem26  31670  fdc  31778  lsatcvat  32325  hlrelat2  32677  ltltncvr  32697  islln2a  32791  islpln2a  32822  islvol2aN  32866  rencldnfilem  35372  ss2iundf  35890  radcnvrat  36300  stoweidlem34  37464  oddneven  38173
  Copyright terms: Public domain W3C validator