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

Theorem mt3d 125
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 124 . 2  |-  ( ph  ->  ( -.  ch  ->  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3i  126  nsyl2  127  ecase23d  1315  disjss3  4279  nnsuc  6482  unxpdomlem2  7506  oismo  7742  cnfcom3lem  7924  cnfcom3lemOLD  7932  rankelb  8019  fin33i  8526  isf34lem4  8534  canthp1lem2  8808  gchcda1  8811  pwfseqlem3  8815  inttsk  8929  r1tskina  8937  nqereu  9086  zbtwnre  10939  discr1  11984  seqcoll2  12201  dvdseq  13563  bitsfzo  13614  bitsf1  13625  eucalglt  13743  4sqlem17  14005  4sqlem18  14006  ramubcl  14062  psgnunilem5  15980  odnncl  16028  gexnnod  16067  sylow1lem1  16077  torsubg  16316  prmcyg  16350  ablfacrplem  16540  pgpfac1lem2  16550  pgpfac1lem3a  16551  pgpfac1lem3  16552  xrsdsreclblem  17703  prmirredlem  17759  prmirredlemOLD  17762  ppttop  18453  pptbas  18454  regr1lem  19154  alexsublem  19458  reconnlem1  20245  metnrmlem1a  20276  vitalilem4  20933  vitalilem5  20934  itg2gt0  21080  rollelem  21303  lhop1lem  21327  coefv0  21600  plyexmo  21664  ppinprm  22375  chtnprm  22377  lgsdir  22554  lgseisenlem1  22573  2sqlem7  22594  2sqblem  22601  pntpbnd1  22720  lgamucov  26872  dfon2lem8  27450  nobndup  27688  nobnddown  27689  nofulllem5  27694  fdc  28485  qirropth  29094  2atm  32744  llnmlplnN  32756  trlval3  33404  cdleme0moN  33442  cdleme18c  33510
  Copyright terms: Public domain W3C validator