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

Theorem con2d 120
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 117 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 33 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 109 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  121  mt2d  122  pm3.2im  150  exists2  2402  necon2bd  2652  spcimegf  3140  spcegf  3142  spcimedv  3145  rspcimedv  3164  minel  3832  disjxun  4414  sotric  4800  sotrieq  4801  poirr2  5243  funun  5643  imadif  5680  soisoi  6244  onnminsb  6658  oneqmin  6659  ordunisuc2  6698  limsssuc  6704  wfrlem10  7071  tz7.48lem  7184  sdomdif  7746  pssinf  7808  unblem1  7849  supnub  8002  infnlb  8034  elirrv  8138  inf3lem6  8164  cantnflem1  8220  cardne  8425  cardsdomel  8434  carddom2  8437  cardmin2  8458  alephnbtwn  8528  infdif2  8666  fin4en1  8765  fin23lem31  8799  isf32lem5  8813  isf34lem4  8833  cfpwsdom  9035  fpwwe2  9094  addnidpi  9352  genpnnp  9456  btwnnz  11041  prime  11045  qsqueeze  11523  xralrple  11527  xmullem2  11580  xmulneg1  11584  ssfzoulel  12036  elfznelfzob  12046  bcval4  12524  seqcoll  12660  hashtpg  12674  swrd0  12827  fsumcvg  13827  fsumsplit  13855  fprodcvg  14033  fprodsplit  14069  dvdsle  14399  divalglem8  14429  bitsinv1lem  14464  pockthg  14899  prmunb  14907  vdwlem6  14985  ramlb  15026  gsumzsplit  17609  opsrtoslem2  18757  obselocv  19340  elcls  20138  fbasrn  20948  ufilb  20970  ufilmax  20971  rnelfmlem  21016  alexsubALTlem4  21114  tsmssplit  21215  recld2  21881  fsumharmonic  23986  chtub  24189  lgsne0  24310  axlowdim  25040  nbusgra  25205  nbgranself  25211  usgrasscusgra  25260  cyclnspth  25408  eupath2lem3  25756  cvnsym  27992  cvntr  27994  atcvati  28088  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemfrcn0  29411  ballotlemirc  29413  ballotlemfrcn0OLD  29449  ballotlemircOLD  29451  dfpo2  30444  sltres  30600  nodenselem5  30623  nocvxminlem  30628  nobndup  30638  nobnddown  30639  nofulllem5  30644  nn0prpw  31028  onsucconi  31146  onint1  31158  icorempt2  31799  relowlpssretop  31812  poimirlem16  32001  poimirlem26  32011  fdc  32119  lsatcvat  32661  hlrelat2  33013  ltltncvr  33033  islln2a  33127  islpln2a  33158  islvol2aN  33202  rencldnfilem  35708  ss2iundf  36296  radcnvrat  36707  stoweidlem34  37933  oddneven  38812  nbgrssovtx  39482  cyclnsPth  39822
  Copyright terms: Public domain W3C validator