Theorem mp3an13 1481

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

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 ⊢ 𝜑
2		mp3an13.2	. . 3 ⊢ 𝜒
3		mp3an13.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1479	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  predeq2  6306  wrecseq2  8318  oeoalem  8587  mulrid  11233  addltmul  12507  fz01en  13609  fznatpl1  13635  expubnd  14244  bernneq  14295  bernneq2  14296  faclbnd4lem1  14359  hashfun  14504  bpoly2  16147  bpoly3  16148  fsumcube  16150  efi4p  16229  efival  16244  cos2tsin  16271  cos01bnd  16278  cos01gt0  16283  dvds0  16365  odd2np1  16435  opoe  16457  divalglem0  16487  gcdid  16621  pythagtriplem4  16915  ressid  17340  fvpr0o  17649  fvpr1o  17650  zringcyg  21683  lecldbas  23445  blssioo  25022  tgioo  25023  rerest  25031  xrrest  25035  zdis  25044  reconnlem2  25055  metdscn2  25085  negcncf  25151  iihalf2  25162  cncmet  25551  rrxmvallem  25633  rrxmval  25634  ovolunlem1a  25725  ismbf3d  25883  c1lip2  26227  pilem2  26685  pilem3  26686  sinperlem  26715  sincosq1sgn  26733  sincosq2sgn  26734  sinq12gt0  26742  cosq14gt0  26745  cosq14ge0  26746  coseq1  26760  sinord  26769  zetacvg  27249  1sgmprm  27433  ppiub  27438  chtublem  27445  chtub  27446  bcp1ctr  27513  bpos1lem  27516  bposlem2  27519  bposlem3  27520  bposlem4  27521  bposlem5  27522  bposlem6  27523  bposlem7  27524  bposlem9  27526  nnsge1  28606  pw2gt0divsd  28708  pw2ge0divsd  28709  pw2ltdivmulsd  28713  pw2ltmuldivs2d  28714  pw2ltdivmuls2d  28720  pw2cut  28723  bdayfinbndlem1  28730  axlowdim  29404  ipidsq  31177  ipasslem1  31298  ipasslem2  31299  ipasslem4  31301  ipasslem5  31302  ipasslem8  31304  ipasslem9  31305  ipasslem11  31307  pjoc1i  31898  h1de2bi  32021  h1de2ctlem  32022  spanunsni  32046  opsqrlem1  32607  opsqrlem6  32612  chrelati  32831  chrelat2i  32832  cvexchlem  32835  pnfinf  33610  1fldgenq  33750  rrhre  34518  erdszelem5  35761  wsuceq2  36380  taupilem1  38060  finxpreclem2  38131  sin2h  38351  cos2h  38352  tan2h  38353  poimirlem27  38383  poimirlem30  38386  broucube  38390  mblfinlem1  38393  heiborlem6  38553  lcmineqlem19  42900  onexomgt  44069  omabs2  44160  icccncfext  46702  dirkertrigeq  46916  pgnbgreunbgrlem4  49022  zlmodzxzel  49272  dignn0flhalflem1  49532  2arymaptfo  49571  fv1prop  49616  fv2prop  49617  line2x  49671  onetansqsecsq  50674  cotsqcscsq  50675