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  1290  disjss3  3962  nnsuc  4610  unxpdomlem2  7001  oismo  7188  cnfcom3lem  7339  rankelb  7429  fin33i  7928  isf34lem4  7936  canthp1lem2  8208  gchcda1  8211  pwfseqlem3  8215  inttsk  8329  r1tskina  8337  nqereu  8486  zbtwnre  10246  discr1  11168  seqcoll2  11332  dvdseq  12503  bitsfzo  12553  bitsf1  12564  eucalglt  12682  4sqlem17  12935  4sqlem18  12936  ramubcl  12992  odnncl  14787  gexnnod  14826  sylow1lem1  14836  torsubg  15073  prmcyg  15107  ablfacrplem  15227  pgpfac1lem2  15237  pgpfac1lem3a  15238  pgpfac1lem3  15239  xrsdsreclblem  16344  prmirredlem  16373  ppttop  16671  pptbas  16672  regr1lem  17357  alexsublem  17665  reconnlem1  18258  metnrmlem1a  18289  vitalilem4  18893  vitalilem5  18894  itg2gt0  19042  rollelem  19263  lhop1lem  19287  coefv0  19556  plyexmo  19620  ppinprm  20317  chtnprm  20319  lgsdir  20496  lgseisenlem1  20515  2sqlem7  20536  2sqblem  20543  pntpbnd1  20662  dfon2lem8  23480  axfelem9  23688  axfelem10  23689  axfelem18  23697  fdc  25787  qirropth  26325  psgnunilem5  26749  2atm  28846  llnmlplnN  28858  trlval3  29506  cdleme0moN  29544  cdleme18c  29612
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator