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  2203  necon3ad  2448  necon2bd  2461  necon4ad  2473  cla4imegf  2800  cla4egf  2802  cla4imedv  2804  rcla4imedv  2823  minel  3417  disjxun  3918  sotric  4233  sotrieq  4234  onnminsb  4486  oneqmin  4487  ordunisuc2  4526  limsssuc  4532  poirr2  4974  funun  5153  imadif  5184  soisoi  5677  tz7.48lem  6339  sdomdif  6894  pssinf  6958  unblem1  6994  supnub  7097  elirrv  7195  inf3lem6  7218  cantnflem1  7275  cardne  7482  cardsdomel  7491  carddom2  7494  cardmin2  7515  alephnbtwn  7582  infdif2  7720  fin4en1  7819  fin23lem31  7853  isf32lem5  7867  isf34lem4  7887  cfpwsdom  8086  fpwwe2  8145  addnidpi  8405  genpnnp  8509  btwnnz  9967  prime  9971  qsqueeze  10406  xralrple  10410  xmullem2  10463  xmulneg1  10467  bcval4  11198  seqcoll  11278  fsumcvg  12062  fsumsplit  12089  dvdsle  12448  divalglem8  12473  bitsinv1lem  12506  pockthg  12827  prmunb  12835  vdwlem6  12907  ramlb  12940  gsumzsplit  15041  opsrtoslem2  16058  obselocv  16460  elcls  16642  fbasrn  17411  ufilb  17433  ufilmax  17434  rnelfmlem  17479  alexsubALTlem4  17576  tsmssplit  17666  recld2  18152  fsumharmonic  20137  chtub  20283  lgsne0  20404  cvnsym  22700  cvntr  22702  atcvati  22796  eupath2lem3  23074  dfpo2  23282  wfrlem10  23433  sltres  23485  axdenselem5  23507  nocvxminlem  23512  axfelem9  23522  axfelem10  23523  axlowdim  23763  onsucconi  24050  onint1  24062  nn0prpw  25405  fdc  25621  rencldnfilem  26069  lsatcvat  27929  hlrelat2  28281  ltltncvr  28301  islln2a  28395  islpln2a  28426  islvol2aN  28470
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator