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  2208  necon3ad  2457  necon2bd  2470  necon4ad  2482  cla4imegf  2837  cla4egf  2839  cla4imedv  2842  rcla4imedv  2861  minel  3485  disjxun  3995  sotric  4312  sotrieq  4313  onnminsb  4567  oneqmin  4568  ordunisuc2  4607  limsssuc  4613  poirr2  5055  funun  5234  imadif  5265  soisoi  5759  tz7.48lem  6421  sdomdif  6977  pssinf  7041  unblem1  7077  supnub  7181  elirrv  7279  inf3lem6  7302  cantnflem1  7359  cardne  7566  cardsdomel  7575  carddom2  7578  cardmin2  7599  alephnbtwn  7666  infdif2  7804  fin4en1  7903  fin23lem31  7937  isf32lem5  7951  isf34lem4  7971  cfpwsdom  8174  fpwwe2  8233  addnidpi  8493  genpnnp  8597  btwnnz  10056  prime  10060  qsqueeze  10495  xralrple  10499  xmullem2  10552  xmulneg1  10556  bcval4  11287  seqcoll  11367  fsumcvg  12151  fsumsplit  12178  dvdsle  12537  divalglem8  12562  bitsinv1lem  12595  pockthg  12916  prmunb  12924  vdwlem6  12996  ramlb  13029  gsumzsplit  15169  opsrtoslem2  16189  obselocv  16591  elcls  16773  fbasrn  17542  ufilb  17564  ufilmax  17565  rnelfmlem  17610  alexsubALTlem4  17707  tsmssplit  17797  recld2  18283  fsumharmonic  20268  chtub  20414  lgsne0  20535  cvnsym  22831  cvntr  22833  atcvati  22927  ballotlemfc0  23013  ballotlemfcc  23014  ballotlemfrcn0  23050  ballotlemirc  23052  eupath2lem3  23276  dfpo2  23484  wfrlem10  23635  sltres  23687  axdenselem5  23709  nocvxminlem  23714  axfelem9  23724  axfelem10  23725  axlowdim  23965  onsucconi  24252  onint1  24264  nn0prpw  25607  fdc  25823  rencldnfilem  26271  stoweidlem34  27152  lsatcvat  28490  hlrelat2  28842  ltltncvr  28862  islln2a  28956  islpln2a  28987  islvol2aN  29031
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator