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

Theorem mp3an13 1412
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 1410 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan 705 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  predeq2  5647  wrecseq2  7363  oeoalem  7628  mulid1  9989  addltmul  11220  eluzaddi  11666  fz01en  12319  fznatpl1  12345  expubnd  12869  bernneq  12938  bernneq2  12939  faclbnd4lem1  13028  hashfun  13172  bpoly2  14724  bpoly3  14725  fsumcube  14727  efi4p  14803  efival  14818  cos2tsin  14845  cos01bnd  14852  cos01gt0  14857  dvds0  14932  odd2np1  15000  opoe  15022  divalglem0  15051  gcdid  15183  pythagtriplem4  15459  ressid  15867  zringcyg  19771  lecldbas  20946  blssioo  22521  tgioo  22522  rerest  22530  xrrest  22533  zdis  22542  reconnlem2  22553  metdscn2  22583  negcncf  22644  iihalf2  22655  cncmet  23042  rrxmvallem  23110  rrxmval  23111  ovolunlem1a  23187  ismbf3d  23344  c1lip2  23682  pilem2  24127  pilem3  24128  sinperlem  24153  sincosq1sgn  24171  sincosq2sgn  24172  sinq12gt0  24180  cosq14gt0  24183  cosq14ge0  24184  coseq1  24195  sinord  24201  zetacvg  24658  1sgmprm  24841  ppiub  24846  chtublem  24853  chtub  24854  bcp1ctr  24921  bpos1lem  24924  bposlem2  24927  bposlem3  24928  bposlem4  24929  bposlem5  24930  bposlem6  24931  bposlem7  24932  bposlem9  24934  axlowdim  25758  ipidsq  27435  ipasslem1  27556  ipasslem2  27557  ipasslem4  27559  ipasslem5  27560  ipasslem8  27562  ipasslem9  27563  ipasslem11  27565  pjoc1i  28160  h1de2bi  28283  h1de2ctlem  28284  spanunsni  28308  opsqrlem1  28869  opsqrlem6  28874  chrelati  29093  chrelat2i  29094  cvexchlem  29097  pnfinf  29546  rrhre  29871  erdszelem5  30920  wsuceq2  31498  taupilem1  32835  finxpreclem2  32894  sin2h  33066  cos2h  33067  tan2h  33068  poimirlem27  33103  poimirlem30  33106  broucube  33110  mblfinlem1  33113  heiborlem6  33282  icccncfext  39431  dirkertrigeq  39651  zlmodzxzel  41447  dignn0flhalflem1  41727  onetansqsecsq  41821  cotsqcscsq  41822
  Copyright terms: Public domain W3C validator