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

Theorem mt3d 125
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 124 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3i  126  nsyl2  127  ecase23d  1327  disjss3  4439  nnsuc  6688  unxpdomlem2  7715  oismo  7954  cnfcom3lem  8136  cnfcom3lemOLD  8144  rankelb  8231  fin33i  8738  isf34lem4  8746  canthp1lem2  9020  gchcda1  9023  pwfseqlem3  9027  inttsk  9141  r1tskina  9149  nqereu  9296  zbtwnre  11169  discr1  12257  seqcoll2  12466  dvdseq  13881  bitsfzo  13933  bitsf1  13944  eucalglt  14062  4sqlem17  14327  4sqlem18  14328  ramubcl  14384  psgnunilem5  16308  odnncl  16358  gexnnod  16397  sylow1lem1  16407  torsubg  16646  prmcyg  16680  ablfacrplem  16899  pgpfac1lem2  16909  pgpfac1lem3a  16910  pgpfac1lem3  16911  xrsdsreclblem  18225  prmirredlem  18283  prmirredlemOLD  18286  ppttop  19267  pptbas  19268  regr1lem  19968  alexsublem  20272  reconnlem1  21059  metnrmlem1a  21090  vitalilem4  21748  vitalilem5  21749  itg2gt0  21895  rollelem  22118  lhop1lem  22142  coefv0  22372  plyexmo  22436  ppinprm  23147  chtnprm  23149  lgsdir  23326  lgseisenlem1  23345  2sqlem7  23366  2sqblem  23373  pntpbnd1  23492  lgamucov  28070  dfon2lem8  28649  nobndup  28887  nobnddown  28888  nofulllem5  28893  fdc  29692  ac6s6  30035  qirropth  30299  2atm  34198  llnmlplnN  34210  trlval3  34858  cdleme0moN  34896  cdleme18c  34964
  Copyright terms: Public domain W3C validator