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

Theorem mp3an13 1443
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 1441 . 2 ((𝜑𝜓) → 𝜃)
51, 4mpan 686 1 (𝜓𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 1081
This theorem is referenced by:  predeq2  6144  wrecseq2  7940  oeoalem  8211  mulid1  10627  addltmul  11861  eluzaddi  12259  fz01en  12923  fznatpl1  12949  expubnd  13529  bernneq  13578  bernneq2  13579  faclbnd4lem1  13641  hashfun  13786  bpoly2  15399  bpoly3  15400  fsumcube  15402  efi4p  15478  efival  15493  cos2tsin  15520  cos01bnd  15527  cos01gt0  15532  dvds0  15613  odd2np1  15678  opoe  15700  divalglem0  15732  gcdid  15863  pythagtriplem4  16144  ressid  16547  fvpr0o  16820  fvpr1o  16821  zringcyg  20566  lecldbas  21755  blssioo  23330  tgioo  23331  rerest  23339  xrrest  23342  zdis  23351  reconnlem2  23362  metdscn2  23392  negcncf  23453  iihalf2  23464  cncmet  23852  rrxmvallem  23934  rrxmval  23935  ovolunlem1a  24024  ismbf3d  24182  c1lip2  24522  pilem2  24967  pilem3  24968  sinperlem  24993  sincosq1sgn  25011  sincosq2sgn  25012  sinq12gt0  25020  cosq14gt0  25023  cosq14ge0  25024  coseq1  25037  sinord  25045  zetacvg  25519  1sgmprm  25702  ppiub  25707  chtublem  25714  chtub  25715  bcp1ctr  25782  bpos1lem  25785  bposlem2  25788  bposlem3  25789  bposlem4  25790  bposlem5  25791  bposlem6  25792  bposlem7  25793  bposlem9  25795  axlowdim  26674  ipidsq  28414  ipasslem1  28535  ipasslem2  28536  ipasslem4  28538  ipasslem5  28539  ipasslem8  28541  ipasslem9  28542  ipasslem11  28544  pjoc1i  29135  h1de2bi  29258  h1de2ctlem  29259  spanunsni  29283  opsqrlem1  29844  opsqrlem6  29849  chrelati  30068  chrelat2i  30069  cvexchlem  30072  pnfinf  30739  rrhre  31161  erdszelem5  32339  wsuceq2  33000  taupilem1  34484  finxpreclem2  34553  sin2h  34763  cos2h  34764  tan2h  34765  poimirlem27  34800  poimirlem30  34803  broucube  34807  mblfinlem1  34810  heiborlem6  34975  icccncfext  42046  dirkertrigeq  42263  zlmodzxzel  44331  dignn0flhalflem1  44603  fv1prop  44614  fv2prop  44615  line2x  44669  onetansqsecsq  44788  cotsqcscsq  44789
  Copyright terms: Public domain W3C validator