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

Theorem mp3an13 1563
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1 𝜑
mp3an13.2 𝜒
mp3an13.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an13 (𝜓𝜃)

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2 𝜑
2 mp3an13.2 . . 3 𝜒
3 mp3an13.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an3 1561 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan 662 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  predeq2  5826  wrecseq2  7563  oeoalem  7830  mulid1  10239  addltmul  11470  eluzaddi  11915  fz01en  12576  fznatpl1  12602  expubnd  13128  bernneq  13197  bernneq2  13198  faclbnd4lem1  13284  hashfun  13426  bpoly2  14994  bpoly3  14995  fsumcube  14997  efi4p  15073  efival  15088  cos2tsin  15115  cos01bnd  15122  cos01gt0  15127  dvds0  15206  odd2np1  15273  opoe  15295  divalglem0  15324  gcdid  15456  pythagtriplem4  15731  ressid  16142  zringcyg  20054  lecldbas  21244  blssioo  22818  tgioo  22819  rerest  22827  xrrest  22830  zdis  22839  reconnlem2  22850  metdscn2  22880  negcncf  22941  iihalf2  22952  cncmet  23338  rrxmvallem  23406  rrxmval  23407  ovolunlem1a  23484  ismbf3d  23641  c1lip2  23981  pilem2  24426  pilem3  24427  pilem3OLD  24428  sinperlem  24453  sincosq1sgn  24471  sincosq2sgn  24472  sinq12gt0  24480  cosq14gt0  24483  cosq14ge0  24484  coseq1  24495  sinord  24501  zetacvg  24962  1sgmprm  25145  ppiub  25150  chtublem  25157  chtub  25158  bcp1ctr  25225  bpos1lem  25228  bposlem2  25231  bposlem3  25232  bposlem4  25233  bposlem5  25234  bposlem6  25235  bposlem7  25236  bposlem9  25238  axlowdim  26062  ipidsq  27905  ipasslem1  28026  ipasslem2  28027  ipasslem4  28029  ipasslem5  28030  ipasslem8  28032  ipasslem9  28033  ipasslem11  28035  pjoc1i  28630  h1de2bi  28753  h1de2ctlem  28754  spanunsni  28778  opsqrlem1  29339  opsqrlem6  29344  chrelati  29563  chrelat2i  29564  cvexchlem  29567  pnfinf  30077  rrhre  30405  erdszelem5  31515  wsuceq2  32098  taupilem1  33504  finxpreclem2  33564  sin2h  33732  cos2h  33733  tan2h  33734  poimirlem27  33769  poimirlem30  33772  broucube  33776  mblfinlem1  33779  heiborlem6  33947  icccncfext  40618  dirkertrigeq  40835  zlmodzxzel  42661  dignn0flhalflem1  42937  onetansqsecsq  43033  cotsqcscsq  43034
  Copyright terms: Public domain W3C validator