Theorem mp3an13 1452

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 1450	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 688	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  predeq2  6220  wrecseq2  8166  oeoalem  8458  mulid1  11019  addltmul  12255  eluzaddi  12657  fz01en  13330  fznatpl1  13356  expubnd  13941  bernneq  13990  bernneq2  13991  faclbnd4lem1  14053  hashfun  14197  bpoly2  15812  bpoly3  15813  fsumcube  15815  efi4p  15891  efival  15906  cos2tsin  15933  cos01bnd  15940  cos01gt0  15945  dvds0  16026  odd2np1  16095  opoe  16117  divalglem0  16147  gcdid  16279  pythagtriplem4  16565  ressid  16999  fvpr0o  17315  fvpr1o  17316  zringcyg  20736  lecldbas  22415  blssioo  24003  tgioo  24004  rerest  24012  xrrest  24015  zdis  24024  reconnlem2  24035  metdscn2  24065  negcncf  24130  iihalf2  24141  cncmet  24531  rrxmvallem  24613  rrxmval  24614  ovolunlem1a  24705  ismbf3d  24863  c1lip2  25207  pilem2  25656  pilem3  25657  sinperlem  25682  sincosq1sgn  25700  sincosq2sgn  25701  sinq12gt0  25709  cosq14gt0  25712  cosq14ge0  25713  coseq1  25726  sinord  25735  zetacvg  26209  1sgmprm  26392  ppiub  26397  chtublem  26404  chtub  26405  bcp1ctr  26472  bpos1lem  26475  bposlem2  26478  bposlem3  26479  bposlem4  26480  bposlem5  26481  bposlem6  26482  bposlem7  26483  bposlem9  26485  axlowdim  27374  ipidsq  29117  ipasslem1  29238  ipasslem2  29239  ipasslem4  29241  ipasslem5  29242  ipasslem8  29244  ipasslem9  29245  ipasslem11  29247  pjoc1i  29838  h1de2bi  29961  h1de2ctlem  29962  spanunsni  29986  opsqrlem1  30547  opsqrlem6  30552  chrelati  30771  chrelat2i  30772  cvexchlem  30775  pnfinf  31482  rrhre  32016  erdszelem5  33202  wsuceq2  33855  taupilem1  35536  finxpreclem2  35605  sin2h  35811  cos2h  35812  tan2h  35813  poimirlem27  35848  poimirlem30  35851  broucube  35855  mblfinlem1  35858  heiborlem6  36018  lcmineqlem19  40097  2xp3dxp2ge1d  40204  icccncfext  43477  dirkertrigeq  43691  zlmodzxzel  45749  dignn0flhalflem1  46019  2arymaptfo  46058  fv1prop  46103  fv2prop  46104  line2x  46158  onetansqsecsq  46521  cotsqcscsq  46522