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  2386  necon3adOLD  2665  necon2bd  2669  necon4adOLD  2675  spcimegf  3185  spcegf  3187  spcimedv  3190  rspcimedv  3209  minel  3870  disjxun  4437  sotric  4815  sotrieq  4816  poirr2  5379  funun  5612  imadif  5645  soisoi  6199  onnminsb  6612  oneqmin  6613  ordunisuc2  6652  limsssuc  6658  tz7.48lem  7098  sdomdif  7658  pssinf  7723  unblem1  7764  supnub  7913  elirrv  8015  inf3lem6  8041  cantnflem1  8099  cantnflem1OLD  8122  cardne  8337  cardsdomel  8346  carddom2  8349  cardmin2  8370  alephnbtwn  8443  infdif2  8581  fin4en1  8680  fin23lem31  8714  isf32lem5  8728  isf34lem4  8748  cfpwsdom  8950  fpwwe2  9010  addnidpi  9268  genpnnp  9372  btwnnz  10935  prime  10939  qsqueeze  11403  xralrple  11407  xmullem2  11460  xmulneg1  11464  ssfzoulel  11887  elfznelfzob  11897  bcval4  12367  seqcoll  12496  hashtpg  12507  swrd0  12650  fsumcvg  13616  fsumsplit  13644  fprodcvg  13819  fprodsplit  13852  dvdsle  14115  divalglem8  14142  bitsinv1lem  14175  pockthg  14508  prmunb  14516  vdwlem6  14588  ramlb  14621  gsumzsplit  17143  gsumzsplitOLD  17144  opsrtoslem2  18344  obselocv  18932  elcls  19741  fbasrn  20551  ufilb  20573  ufilmax  20574  rnelfmlem  20619  alexsubALTlem4  20716  tsmssplit  20820  recld2  21485  fsumharmonic  23539  chtub  23685  lgsne0  23806  axlowdim  24466  nbusgra  24630  nbgranself  24636  usgrasscusgra  24685  cyclnspth  24833  eupath2lem3  25181  cvnsym  27407  cvntr  27409  atcvati  27503  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemfrcn0  28732  ballotlemirc  28734  dfpo2  29425  wfrlem10  29592  sltres  29664  nodenselem5  29685  nocvxminlem  29690  nobndup  29700  nobnddown  29701  nofulllem5  29706  onsucconi  30130  onint1  30142  nn0prpw  30381  fdc  30478  rencldnfilem  30993  radcnvrat  31436  stoweidlem34  32055  oddneven  32558  lsatcvat  35172  hlrelat2  35524  ltltncvr  35544  islln2a  35638  islpln2a  35669  islvol2aN  35713
  Copyright terms: Public domain W3C validator