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 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3i  120  nsyl2  121  ecase23d  1287  disjss3  4153  nnsuc  4803  unxpdomlem2  7251  oismo  7443  cnfcom3lem  7594  rankelb  7684  fin33i  8183  isf34lem4  8191  canthp1lem2  8462  gchcda1  8465  pwfseqlem3  8469  inttsk  8583  r1tskina  8591  nqereu  8740  zbtwnre  10505  discr1  11443  seqcoll2  11641  dvdseq  12825  bitsfzo  12875  bitsf1  12886  eucalglt  13004  4sqlem17  13257  4sqlem18  13258  ramubcl  13314  odnncl  15111  gexnnod  15150  sylow1lem1  15160  torsubg  15397  prmcyg  15431  ablfacrplem  15551  pgpfac1lem2  15561  pgpfac1lem3a  15562  pgpfac1lem3  15563  xrsdsreclblem  16668  prmirredlem  16697  ppttop  16995  pptbas  16996  regr1lem  17693  alexsublem  17997  reconnlem1  18729  metnrmlem1a  18760  vitalilem4  19371  vitalilem5  19372  itg2gt0  19520  rollelem  19741  lhop1lem  19765  coefv0  20034  plyexmo  20098  ppinprm  20803  chtnprm  20805  lgsdir  20982  lgseisenlem1  21001  2sqlem7  21022  2sqblem  21029  pntpbnd1  21148  lgamucov  24602  dfon2lem8  25171  nobndup  25379  nobnddown  25380  nofulllem5  25385  fdc  26141  qirropth  26663  psgnunilem5  27087  2atm  29642  llnmlplnN  29654  trlval3  30302  cdleme0moN  30340  cdleme18c  30408
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator