MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt3d Structured version   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  4203  nnsuc  4854  unxpdomlem2  7306  oismo  7499  cnfcom3lem  7650  rankelb  7740  fin33i  8239  isf34lem4  8247  canthp1lem2  8518  gchcda1  8521  pwfseqlem3  8525  inttsk  8639  r1tskina  8647  nqereu  8796  zbtwnre  10562  discr1  11505  seqcoll2  11703  dvdseq  12887  bitsfzo  12937  bitsf1  12948  eucalglt  13066  4sqlem17  13319  4sqlem18  13320  ramubcl  13376  odnncl  15173  gexnnod  15212  sylow1lem1  15222  torsubg  15459  prmcyg  15493  ablfacrplem  15613  pgpfac1lem2  15623  pgpfac1lem3a  15624  pgpfac1lem3  15625  xrsdsreclblem  16734  prmirredlem  16763  ppttop  17061  pptbas  17062  regr1lem  17761  alexsublem  18065  reconnlem1  18847  metnrmlem1a  18878  vitalilem4  19493  vitalilem5  19494  itg2gt0  19642  rollelem  19863  lhop1lem  19887  coefv0  20156  plyexmo  20220  ppinprm  20925  chtnprm  20927  lgsdir  21104  lgseisenlem1  21123  2sqlem7  21144  2sqblem  21151  pntpbnd1  21270  lgamucov  24812  dfon2lem8  25405  nobndup  25620  nobnddown  25621  nofulllem5  25626  fdc  26403  qirropth  26925  psgnunilem5  27349  2atm  30225  llnmlplnN  30237  trlval3  30885  cdleme0moN  30923  cdleme18c  30991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator