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

Theorem con2d 107
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 104 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 28 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 97 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con2  108  mt2d  109  pm3.2im  137  exists2  2234  necon3ad  2483  necon2bd  2496  necon4ad  2508  spcimegf  2863  spcegf  2865  spcimedv  2868  rspcimedv  2887  minel  3511  disjxun  4022  sotric  4339  sotrieq  4340  onnminsb  4594  oneqmin  4595  ordunisuc2  4634  limsssuc  4640  poirr2  5066  funun  5262  imadif  5293  soisoi  5787  tz7.48lem  6449  sdomdif  7005  pssinf  7069  unblem1  7105  supnub  7209  elirrv  7307  inf3lem6  7330  cantnflem1  7387  cardne  7594  cardsdomel  7603  carddom2  7606  cardmin2  7627  alephnbtwn  7694  infdif2  7832  fin4en1  7931  fin23lem31  7965  isf32lem5  7979  isf34lem4  7999  cfpwsdom  8202  fpwwe2  8261  addnidpi  8521  genpnnp  8625  btwnnz  10084  prime  10088  qsqueeze  10524  xralrple  10528  xmullem2  10581  xmulneg1  10585  bcval4  11316  seqcoll  11397  fsumcvg  12181  fsumsplit  12208  dvdsle  12570  divalglem8  12595  bitsinv1lem  12628  pockthg  12949  prmunb  12957  vdwlem6  13029  ramlb  13062  gsumzsplit  15202  opsrtoslem2  16222  obselocv  16624  elcls  16806  fbasrn  17575  ufilb  17597  ufilmax  17598  rnelfmlem  17643  alexsubALTlem4  17740  tsmssplit  17830  recld2  18316  fsumharmonic  20301  chtub  20447  lgsne0  20568  cvnsym  22866  cvntr  22868  atcvati  22962  ballotlemfc0  23047  ballotlemfcc  23048  ballotlemfrcn0  23084  ballotlemirc  23086  eupath2lem3  23310  dfpo2  23518  wfrlem10  23669  sltres  23721  axdenselem5  23743  nocvxminlem  23748  axfelem9  23758  axfelem10  23759  axlowdim  23999  onsucconi  24286  onint1  24298  nn0prpw  25650  fdc  25866  rencldnfilem  26314  stoweidlem34  27194  lsatcvat  28519  hlrelat2  28871  ltltncvr  28891  islln2a  28985  islpln2a  29016  islvol2aN  29060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator