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

Theorem mp3an13 1305
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1  |-  ph
mp3an13.2  |-  ch
mp3an13.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an13  |-  ( ps 
->  th )

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2  |-  ph
2 mp3an13.2 . . 3  |-  ch
3 mp3an13.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1303 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 670 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  oeoalem  7040  mulid1  9388  addltmul  10565  uzindOLD  10741  eluzaddi  10892  fz01en  11482  fznatpl1  11515  expubnd  11929  bernneq  11995  bernneq2  11996  faclbnd4lem1  12074  hashfun  12204  efi4p  13426  efival  13441  cos2tsin  13468  cos01bnd  13475  cos01gt0  13480  dvds0  13553  odd2np1  13597  divalglem0  13602  gcdid  13720  opoe  13883  pythagtriplem4  13891  ressid  14238  zringcyg  17912  zcyg  17917  lecldbas  18828  blssioo  20377  tgioo  20378  rerest  20386  xrrest  20389  zdis  20398  reconnlem2  20409  metdscn2  20438  negcncf  20499  iihalf2  20510  cncmet  20838  rrxmvallem  20908  rrxmval  20909  ovolunlem1a  20984  ismbf3d  21137  c1lip2  21475  pilem2  21922  pilem3  21923  sinperlem  21947  sincosq1sgn  21965  sincosq2sgn  21966  sinq12gt0  21974  cosq14gt0  21977  cosq14ge0  21978  coseq1  21989  sinord  21995  1sgmprm  22543  ppiub  22548  chtublem  22555  chtub  22556  bcp1ctr  22623  bpos1lem  22626  bposlem2  22629  bposlem3  22630  bposlem4  22631  bposlem5  22632  bposlem6  22633  bposlem7  22634  bposlem9  22636  axlowdim  23212  2trllemD  23461  2trllemG  23462  constr1trl  23492  constr3lem4  23538  ipidsq  24113  ipasslem1  24236  ipasslem2  24237  ipasslem4  24239  ipasslem5  24240  ipasslem8  24242  ipasslem9  24243  ipasslem11  24245  pjoc1i  24839  h1de2bi  24962  h1de2ctlem  24963  spanunsni  24987  opsqrlem1  25549  opsqrlem6  25554  chrelati  25773  chrelat2i  25774  cvexchlem  25777  pnfinf  26205  rrhre  26452  zetacvg  27006  erdszelem5  27088  predeq2  27633  wrecseq2  27726  wsuceq2  27758  bpoly2  28205  bpoly3  28206  fsumcube  28208  sin2h  28427  cos2h  28428  tan2h  28429  mblfinlem1  28433  heiborlem6  28720  zlmodzxzel  30757  onetansqsecsq  31101  cotsqcscsq  31102  taupilem1  35620
  Copyright terms: Public domain W3C validator