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  4171  nnsuc  4821  unxpdomlem2  7273  oismo  7465  cnfcom3lem  7616  rankelb  7706  fin33i  8205  isf34lem4  8213  canthp1lem2  8484  gchcda1  8487  pwfseqlem3  8491  inttsk  8605  r1tskina  8613  nqereu  8762  zbtwnre  10528  discr1  11470  seqcoll2  11668  dvdseq  12852  bitsfzo  12902  bitsf1  12913  eucalglt  13031  4sqlem17  13284  4sqlem18  13285  ramubcl  13341  odnncl  15138  gexnnod  15177  sylow1lem1  15187  torsubg  15424  prmcyg  15458  ablfacrplem  15578  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  xrsdsreclblem  16699  prmirredlem  16728  ppttop  17026  pptbas  17027  regr1lem  17724  alexsublem  18028  reconnlem1  18810  metnrmlem1a  18841  vitalilem4  19456  vitalilem5  19457  itg2gt0  19605  rollelem  19826  lhop1lem  19850  coefv0  20119  plyexmo  20183  ppinprm  20888  chtnprm  20890  lgsdir  21067  lgseisenlem1  21086  2sqlem7  21107  2sqblem  21114  pntpbnd1  21233  lgamucov  24775  dfon2lem8  25360  nobndup  25568  nobnddown  25569  nofulllem5  25574  fdc  26339  qirropth  26861  psgnunilem5  27285  2atm  30009  llnmlplnN  30021  trlval3  30669  cdleme0moN  30707  cdleme18c  30775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator