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  1323  disjss3  4389  nnsuc  6593  unxpdomlem2  7619  oismo  7855  cnfcom3lem  8037  cnfcom3lemOLD  8045  rankelb  8132  fin33i  8639  isf34lem4  8647  canthp1lem2  8921  gchcda1  8924  pwfseqlem3  8928  inttsk  9042  r1tskina  9050  nqereu  9199  zbtwnre  11052  discr1  12101  seqcoll2  12319  dvdseq  13682  bitsfzo  13733  bitsf1  13744  eucalglt  13862  4sqlem17  14124  4sqlem18  14125  ramubcl  14181  psgnunilem5  16102  odnncl  16152  gexnnod  16191  sylow1lem1  16201  torsubg  16440  prmcyg  16474  ablfacrplem  16671  pgpfac1lem2  16681  pgpfac1lem3a  16682  pgpfac1lem3  16683  xrsdsreclblem  17968  prmirredlem  18026  prmirredlemOLD  18029  ppttop  18727  pptbas  18728  regr1lem  19428  alexsublem  19732  reconnlem1  20519  metnrmlem1a  20550  vitalilem4  21207  vitalilem5  21208  itg2gt0  21354  rollelem  21577  lhop1lem  21601  coefv0  21831  plyexmo  21895  ppinprm  22606  chtnprm  22608  lgsdir  22785  lgseisenlem1  22804  2sqlem7  22825  2sqblem  22832  pntpbnd1  22951  lgamucov  27158  dfon2lem8  27737  nobndup  27975  nobnddown  27976  nofulllem5  27981  fdc  28779  ac6s6  29122  qirropth  29387  2atm  33477  llnmlplnN  33489  trlval3  34137  cdleme0moN  34175  cdleme18c  34243
  Copyright terms: Public domain W3C validator