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

Theorem mp3an13 1445
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 1443 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan 686 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  predeq2  6148  wrecseq2  7945  oeoalem  8215  mulid1  10631  addltmul  11865  eluzaddi  12263  fz01en  12928  fznatpl1  12954  expubnd  13534  bernneq  13583  bernneq2  13584  faclbnd4lem1  13646  hashfun  13791  bpoly2  15403  bpoly3  15404  fsumcube  15406  efi4p  15482  efival  15497  cos2tsin  15524  cos01bnd  15531  cos01gt0  15536  dvds0  15617  odd2np1  15682  opoe  15704  divalglem0  15736  gcdid  15867  pythagtriplem4  16148  ressid  16551  fvpr0o  16824  fvpr1o  16825  zringcyg  20556  lecldbas  21745  blssioo  23320  tgioo  23321  rerest  23329  xrrest  23332  zdis  23341  reconnlem2  23352  metdscn2  23382  negcncf  23443  iihalf2  23454  cncmet  23842  rrxmvallem  23924  rrxmval  23925  ovolunlem1a  24014  ismbf3d  24172  c1lip2  24512  pilem2  24957  pilem3  24958  sinperlem  24983  sincosq1sgn  25001  sincosq2sgn  25002  sinq12gt0  25010  cosq14gt0  25013  cosq14ge0  25014  coseq1  25027  sinord  25033  zetacvg  25508  1sgmprm  25691  ppiub  25696  chtublem  25703  chtub  25704  bcp1ctr  25771  bpos1lem  25774  bposlem2  25777  bposlem3  25778  bposlem4  25779  bposlem5  25780  bposlem6  25781  bposlem7  25782  bposlem9  25784  axlowdim  26663  ipidsq  28403  ipasslem1  28524  ipasslem2  28525  ipasslem4  28527  ipasslem5  28528  ipasslem8  28530  ipasslem9  28531  ipasslem11  28533  pjoc1i  29124  h1de2bi  29247  h1de2ctlem  29248  spanunsni  29272  opsqrlem1  29833  opsqrlem6  29838  chrelati  30057  chrelat2i  30058  cvexchlem  30061  pnfinf  30728  rrhre  31150  erdszelem5  32328  wsuceq2  32989  taupilem1  34473  finxpreclem2  34542  sin2h  34751  cos2h  34752  tan2h  34753  poimirlem27  34788  poimirlem30  34791  broucube  34795  mblfinlem1  34798  heiborlem6  34964  icccncfext  42037  dirkertrigeq  42254  zlmodzxzel  44237  dignn0flhalflem1  44509  fv1prop  44520  fv2prop  44521  line2x  44575  onetansqsecsq  44694  cotsqcscsq  44695
  Copyright terms: Public domain W3C validator