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 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt3i  120  nsyl2  121  ecase23d  1287  disjss3  4024  nnsuc  4673  unxpdomlem2  7064  oismo  7251  cnfcom3lem  7402  rankelb  7492  fin33i  7991  isf34lem4  7999  canthp1lem2  8271  gchcda1  8274  pwfseqlem3  8278  inttsk  8392  r1tskina  8400  nqereu  8549  zbtwnre  10310  discr1  11232  seqcoll2  11397  dvdseq  12571  bitsfzo  12621  bitsf1  12632  eucalglt  12750  4sqlem17  13003  4sqlem18  13004  ramubcl  13060  odnncl  14855  gexnnod  14894  sylow1lem1  14904  torsubg  15141  prmcyg  15175  ablfacrplem  15295  pgpfac1lem2  15305  pgpfac1lem3a  15306  pgpfac1lem3  15307  xrsdsreclblem  16412  prmirredlem  16441  ppttop  16739  pptbas  16740  regr1lem  17425  alexsublem  17733  reconnlem1  18326  metnrmlem1a  18357  vitalilem4  18961  vitalilem5  18962  itg2gt0  19110  rollelem  19331  lhop1lem  19355  coefv0  19624  plyexmo  19688  ppinprm  20385  chtnprm  20387  lgsdir  20564  lgseisenlem1  20583  2sqlem7  20604  2sqblem  20611  pntpbnd1  20730  dfon2lem8  23548  axfelem9  23756  axfelem10  23757  axfelem18  23765  fdc  25855  qirropth  26393  psgnunilem5  26817  2atm  28984  llnmlplnN  28996  trlval3  29644  cdleme0moN  29682  cdleme18c  29750
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator