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

Theorem mt3d 119
Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
Hypotheses
Ref Expression
mt3d.1  |-  ( ph  ->  -.  ch )
mt3d.2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
Assertion
Ref Expression
mt3d  |-  ( ph  ->  ps )

Proof of Theorem mt3d
StepHypRef Expression
1 mt3d.1 . 2  |-  ( ph  ->  -.  ch )
2 mt3d.2 . . 3  |-  ( ph  ->  ( -.  ps  ->  ch ) )
32con1d 118 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3i  120  nsyl2  121  ecase23d  1290  disjss3  3919  nnsuc  4564  unxpdomlem2  6953  oismo  7139  cnfcom3lem  7290  rankelb  7380  fin33i  7879  isf34lem4  7887  canthp1lem2  8155  gchcda1  8158  pwfseqlem3  8162  inttsk  8276  r1tskina  8284  nqereu  8433  zbtwnre  10193  discr1  11115  seqcoll2  11279  dvdseq  12450  bitsfzo  12500  bitsf1  12511  eucalglt  12629  4sqlem17  12882  4sqlem18  12883  ramubcl  12939  odnncl  14695  gexnnod  14734  sylow1lem1  14744  torsubg  14981  prmcyg  15015  ablfacrplem  15135  pgpfac1lem2  15145  pgpfac1lem3a  15146  pgpfac1lem3  15147  xrsdsreclblem  16249  prmirredlem  16278  ppttop  16576  pptbas  16577  regr1lem  17262  alexsublem  17570  reconnlem1  18163  metnrmlem1a  18194  vitalilem4  18798  vitalilem5  18799  itg2gt0  18947  rollelem  19168  lhop1lem  19192  coefv0  19461  plyexmo  19525  ppinprm  20222  chtnprm  20224  lgsdir  20401  lgseisenlem1  20420  2sqlem7  20441  2sqblem  20448  pntpbnd1  20567  dfon2lem8  23314  axfelem9  23522  axfelem10  23523  axfelem18  23531  fdc  25621  qirropth  26159  psgnunilem5  26583  2atm  28405  llnmlplnN  28417  trlval3  29065  cdleme0moN  29103  cdleme18c  29171
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator