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

Theorem mt3d 117
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 116 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt3i  118  nsyl2  119  ecase23d  1285  disjss3  4038  nnsuc  4689  unxpdomlem2  7084  oismo  7271  cnfcom3lem  7422  rankelb  7512  fin33i  8011  isf34lem4  8019  canthp1lem2  8291  gchcda1  8294  pwfseqlem3  8298  inttsk  8412  r1tskina  8420  nqereu  8569  zbtwnre  10330  discr1  11253  seqcoll2  11418  dvdseq  12592  bitsfzo  12642  bitsf1  12653  eucalglt  12771  4sqlem17  13024  4sqlem18  13025  ramubcl  13081  odnncl  14876  gexnnod  14915  sylow1lem1  14925  torsubg  15162  prmcyg  15196  ablfacrplem  15316  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  xrsdsreclblem  16433  prmirredlem  16462  ppttop  16760  pptbas  16761  regr1lem  17446  alexsublem  17754  reconnlem1  18347  metnrmlem1a  18378  vitalilem4  18982  vitalilem5  18983  itg2gt0  19131  rollelem  19352  lhop1lem  19376  coefv0  19645  plyexmo  19709  ppinprm  20406  chtnprm  20408  lgsdir  20585  lgseisenlem1  20604  2sqlem7  20625  2sqblem  20632  pntpbnd1  20751  dfon2lem8  24217  nobndup  24425  nobnddown  24426  nofulllem5  24431  fdc  26558  qirropth  27096  psgnunilem5  27520  2atm  30338  llnmlplnN  30350  trlval3  30998  cdleme0moN  31036  cdleme18c  31104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator