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  4022  nnsuc  4673  unxpdomlem2  7068  oismo  7255  cnfcom3lem  7406  rankelb  7496  fin33i  7995  isf34lem4  8003  canthp1lem2  8275  gchcda1  8278  pwfseqlem3  8282  inttsk  8396  r1tskina  8404  nqereu  8553  zbtwnre  10314  discr1  11237  seqcoll2  11402  dvdseq  12576  bitsfzo  12626  bitsf1  12637  eucalglt  12755  4sqlem17  13008  4sqlem18  13009  ramubcl  13065  odnncl  14860  gexnnod  14899  sylow1lem1  14909  torsubg  15146  prmcyg  15180  ablfacrplem  15300  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  xrsdsreclblem  16417  prmirredlem  16446  ppttop  16744  pptbas  16745  regr1lem  17430  alexsublem  17738  reconnlem1  18331  metnrmlem1a  18362  vitalilem4  18966  vitalilem5  18967  itg2gt0  19115  rollelem  19336  lhop1lem  19360  coefv0  19629  plyexmo  19693  ppinprm  20390  chtnprm  20392  lgsdir  20569  lgseisenlem1  20588  2sqlem7  20609  2sqblem  20616  pntpbnd1  20735  dfon2lem8  24146  nobndup  24354  nobnddown  24355  nofulllem5  24360  fdc  26455  qirropth  26993  psgnunilem5  27417  2atm  29716  llnmlplnN  29728  trlval3  30376  cdleme0moN  30414  cdleme18c  30482
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator