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  2813  cla4egf  2815  cla4imedv  2818  rcla4imedv  2837  minel  3452  disjxun  3961  sotric  4277  sotrieq  4278  onnminsb  4532  oneqmin  4533  ordunisuc2  4572  limsssuc  4578  poirr2  5020  funun  5199  imadif  5230  soisoi  5724  tz7.48lem  6386  sdomdif  6942  pssinf  7006  unblem1  7042  supnub  7146  elirrv  7244  inf3lem6  7267  cantnflem1  7324  cardne  7531  cardsdomel  7540  carddom2  7543  cardmin2  7564  alephnbtwn  7631  infdif2  7769  fin4en1  7868  fin23lem31  7902  isf32lem5  7916  isf34lem4  7936  cfpwsdom  8139  fpwwe2  8198  addnidpi  8458  genpnnp  8562  btwnnz  10020  prime  10024  qsqueeze  10459  xralrple  10463  xmullem2  10516  xmulneg1  10520  bcval4  11251  seqcoll  11331  fsumcvg  12115  fsumsplit  12142  dvdsle  12501  divalglem8  12526  bitsinv1lem  12559  pockthg  12880  prmunb  12888  vdwlem6  12960  ramlb  12993  gsumzsplit  15133  opsrtoslem2  16153  obselocv  16555  elcls  16737  fbasrn  17506  ufilb  17528  ufilmax  17529  rnelfmlem  17574  alexsubALTlem4  17671  tsmssplit  17761  recld2  18247  fsumharmonic  20232  chtub  20378  lgsne0  20499  cvnsym  22795  cvntr  22797  atcvati  22891  ballotlemfc0  22977  ballotlemfcc  22978  ballotlemfrcn0  23014  ballotlemirc  23016  eupath2lem3  23240  dfpo2  23448  wfrlem10  23599  sltres  23651  axdenselem5  23673  nocvxminlem  23678  axfelem9  23688  axfelem10  23689  axlowdim  23929  onsucconi  24216  onint1  24228  nn0prpw  25571  fdc  25787  rencldnfilem  26235  stoweidlem34  27083  lsatcvat  28370  hlrelat2  28722  ltltncvr  28742  islln2a  28836  islpln2a  28867  islvol2aN  28911
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator