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

Theorem con2d 109
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 106 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con2d.1 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
31, 2syl5 30 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  -.  ch ) )
43con4d 99 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  con2  110  mt2d  111  pm3.2im  139  exists2  2206  necon3ad  2455  necon2bd  2468  necon4ad  2480  cla4imegf  2830  cla4egf  2832  cla4imedv  2835  rcla4imedv  2854  minel  3471  disjxun  3981  sotric  4298  sotrieq  4299  onnminsb  4553  oneqmin  4554  ordunisuc2  4593  limsssuc  4599  poirr2  5041  funun  5220  imadif  5251  soisoi  5745  tz7.48lem  6407  sdomdif  6963  pssinf  7027  unblem1  7063  supnub  7167  elirrv  7265  inf3lem6  7288  cantnflem1  7345  cardne  7552  cardsdomel  7561  carddom2  7564  cardmin2  7585  alephnbtwn  7652  infdif2  7790  fin4en1  7889  fin23lem31  7923  isf32lem5  7937  isf34lem4  7957  cfpwsdom  8160  fpwwe2  8219  addnidpi  8479  genpnnp  8583  btwnnz  10041  prime  10045  qsqueeze  10480  xralrple  10484  xmullem2  10537  xmulneg1  10541  bcval4  11272  seqcoll  11352  fsumcvg  12136  fsumsplit  12163  dvdsle  12522  divalglem8  12547  bitsinv1lem  12580  pockthg  12901  prmunb  12909  vdwlem6  12981  ramlb  13014  gsumzsplit  15154  opsrtoslem2  16174  obselocv  16576  elcls  16758  fbasrn  17527  ufilb  17549  ufilmax  17550  rnelfmlem  17595  alexsubALTlem4  17692  tsmssplit  17782  recld2  18268  fsumharmonic  20253  chtub  20399  lgsne0  20520  cvnsym  22816  cvntr  22818  atcvati  22912  ballotlemfc0  22998  ballotlemfcc  22999  ballotlemfrcn0  23035  ballotlemirc  23037  eupath2lem3  23261  dfpo2  23469  wfrlem10  23620  sltres  23672  axdenselem5  23694  nocvxminlem  23699  axfelem9  23709  axfelem10  23710  axlowdim  23950  onsucconi  24237  onint1  24249  nn0prpw  25592  fdc  25808  rencldnfilem  26256  stoweidlem34  27104  lsatcvat  28391  hlrelat2  28743  ltltncvr  28763  islln2a  28857  islpln2a  28888  islvol2aN  28932
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator