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

Theorem mp3an13 1270
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 1268 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 652 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  oeoalem  6798  mulid1  9044  addltmul  10159  uzindOLD  10320  eluzaddi  10468  fz01en  11035  expubnd  11395  bernneq  11460  bernneq2  11461  faclbnd4lem1  11539  hashfun  11655  efi4p  12693  efival  12708  cos2tsin  12735  cos01bnd  12742  cos01gt0  12747  dvds0  12820  odd2np1  12863  divalglem0  12868  gcdid  12986  opoe  13140  pythagtriplem4  13148  ressid  13479  zcyg  16727  lecldbas  17237  blssioo  18779  tgioo  18780  rerest  18788  xrrest  18791  zdis  18800  reconnlem2  18811  metdscn2  18840  negcncf  18901  iihalf2  18911  cncmet  19228  ovolunlem1a  19345  ismbf3d  19499  c1lip2  19835  pilem2  20321  pilem3  20322  sinperlem  20341  sincosq1sgn  20359  sincosq2sgn  20360  sinq12gt0  20368  cosq14gt0  20371  cosq14ge0  20372  coseq1  20383  sinord  20389  1sgmprm  20936  ppiub  20941  chtublem  20948  chtub  20949  bcp1ctr  21016  bpos1lem  21019  bposlem2  21022  bposlem3  21023  bposlem4  21024  bposlem5  21025  bposlem6  21026  bposlem7  21027  bposlem9  21029  2trllemD  21510  2trllemG  21511  constr1trl  21541  constr3lem4  21587  ipidsq  22162  ipasslem1  22285  ipasslem2  22286  ipasslem4  22288  ipasslem5  22289  ipasslem8  22291  ipasslem9  22292  ipasslem11  22294  pjoc1i  22886  h1de2bi  23009  h1de2ctlem  23010  spanunsni  23034  opsqrlem1  23596  opsqrlem6  23601  chrelati  23820  chrelat2i  23821  cvexchlem  23824  pnfinf  24206  rrhre  24340  zetacvg  24752  erdszelem5  24834  fznatpl1  25151  axlowdim  25804  bpoly2  26007  bpoly3  26008  fsumcube  26010  mblfinlem  26143  heiborlem6  26415  onetansqsecsq  28218  cotsqcscsq  28219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator