Theorem mp3an13 1528

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

Syntax hints:   → wi 4   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  predeq2  5796  wrecseq2  7531  oeoalem  7796  mulid1  10150  addltmul  11381  eluzaddi  11827  fz01en  12483  fznatpl1  12509  expubnd  13036  bernneq  13105  bernneq2  13106  faclbnd4lem1  13195  hashfun  13337  bpoly2  14908  bpoly3  14909  fsumcube  14911  efi4p  14987  efival  15002  cos2tsin  15029  cos01bnd  15036  cos01gt0  15041  dvds0  15120  odd2np1  15188  opoe  15210  divalglem0  15239  gcdid  15371  pythagtriplem4  15647  ressid  16058  zringcyg  19962  lecldbas  21146  blssioo  22720  tgioo  22721  rerest  22729  xrrest  22732  zdis  22741  reconnlem2  22752  metdscn2  22782  negcncf  22843  iihalf2  22854  cncmet  23240  rrxmvallem  23308  rrxmval  23309  ovolunlem1a  23385  ismbf3d  23541  c1lip2  23881  pilem2  24326  pilem3  24327  sinperlem  24352  sincosq1sgn  24370  sincosq2sgn  24371  sinq12gt0  24379  cosq14gt0  24382  cosq14ge0  24383  coseq1  24394  sinord  24400  zetacvg  24861  1sgmprm  25044  ppiub  25049  chtublem  25056  chtub  25057  bcp1ctr  25124  bpos1lem  25127  bposlem2  25130  bposlem3  25131  bposlem4  25132  bposlem5  25133  bposlem6  25134  bposlem7  25135  bposlem9  25137  axlowdim  25961  ipidsq  27795  ipasslem1  27916  ipasslem2  27917  ipasslem4  27919  ipasslem5  27920  ipasslem8  27922  ipasslem9  27923  ipasslem11  27925  pjoc1i  28520  h1de2bi  28643  h1de2ctlem  28644  spanunsni  28668  opsqrlem1  29229  opsqrlem6  29234  chrelati  29453  chrelat2i  29454  cvexchlem  29457  pnfinf  29967  rrhre  30295  erdszelem5  31405  wsuceq2  31988  taupilem1  33399  finxpreclem2  33459  sin2h  33631  cos2h  33632  tan2h  33633  poimirlem27  33668  poimirlem30  33671  broucube  33675  mblfinlem1  33678  heiborlem6  33847  icccncfext  40520  dirkertrigeq  40738  zlmodzxzel  42560  dignn0flhalflem1  42836  onetansqsecsq  42932  cotsqcscsq  42933