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  1331  disjss3  4432  nnsuc  6698  unxpdomlem2  7723  oismo  7963  cnfcom3lem  8145  cnfcom3lemOLD  8153  rankelb  8240  fin33i  8747  isf34lem4  8755  canthp1lem2  9029  gchcda1  9032  pwfseqlem3  9036  inttsk  9150  r1tskina  9158  nqereu  9305  zbtwnre  11184  discr1  12276  seqcoll2  12487  dvdseq  13905  bitsfzo  13957  bitsf1  13968  eucalglt  14086  4sqlem17  14351  4sqlem18  14352  ramubcl  14408  psgnunilem5  16388  odnncl  16438  gexnnod  16477  sylow1lem1  16487  torsubg  16729  prmcyg  16765  ablfacrplem  16984  pgpfac1lem2  16994  pgpfac1lem3a  16995  pgpfac1lem3  16996  xrsdsreclblem  18332  prmirredlem  18390  prmirredlemOLD  18393  ppttop  19374  pptbas  19375  regr1lem  20106  alexsublem  20410  reconnlem1  21197  metnrmlem1a  21228  vitalilem4  21886  vitalilem5  21887  itg2gt0  22033  rollelem  22256  lhop1lem  22280  coefv0  22510  plyexmo  22574  ppinprm  23291  chtnprm  23293  lgsdir  23470  lgseisenlem1  23489  2sqlem7  23510  2sqblem  23517  pntpbnd1  23636  lgamucov  28446  dfon2lem8  29190  nobndup  29428  nobnddown  29429  nofulllem5  29434  fdc  30206  ac6s6  30548  qirropth  30812  2atm  34953  llnmlplnN  34965  trlval3  35614  cdleme0moN  35652  cdleme18c  35720
  Copyright terms: Public domain W3C validator