Theorem mp3an13 1407

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

Syntax hints:   → wi 4   ∧ w3a 1031

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

This theorem is referenced by:  predeq2  5600  wrecseq2  7298  oeoalem  7563  mulid1  9916  addltmul  11145  eluzaddi  11590  fz01en  12240  fznatpl1  12265  expubnd  12783  bernneq  12852  bernneq2  12853  faclbnd4lem1  12942  hashfun  13084  bpoly2  14627  bpoly3  14628  fsumcube  14630  efi4p  14706  efival  14721  cos2tsin  14748  cos01bnd  14755  cos01gt0  14760  dvds0  14835  odd2np1  14903  opoe  14925  divalglem0  14954  gcdid  15086  pythagtriplem4  15362  ressid  15762  zringcyg  19658  lecldbas  20833  blssioo  22406  tgioo  22407  rerest  22415  xrrest  22418  zdis  22427  reconnlem2  22438  metdscn2  22468  negcncf  22529  iihalf2  22540  cncmet  22927  rrxmvallem  22995  rrxmval  22996  ovolunlem1a  23071  ismbf3d  23227  c1lip2  23565  pilem2  24010  pilem3  24011  sinperlem  24036  sincosq1sgn  24054  sincosq2sgn  24055  sinq12gt0  24063  cosq14gt0  24066  cosq14ge0  24067  coseq1  24078  sinord  24084  zetacvg  24541  1sgmprm  24724  ppiub  24729  chtublem  24736  chtub  24737  bcp1ctr  24804  bpos1lem  24807  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem9  24817  axlowdim  25641  2trllemD  26087  2trllemG  26088  constr1trl  26118  constr3lem4  26175  ipidsq  26949  ipasslem1  27070  ipasslem2  27071  ipasslem4  27073  ipasslem5  27074  ipasslem8  27076  ipasslem9  27077  ipasslem11  27079  pjoc1i  27674  h1de2bi  27797  h1de2ctlem  27798  spanunsni  27822  opsqrlem1  28383  opsqrlem6  28388  chrelati  28607  chrelat2i  28608  cvexchlem  28611  pnfinf  29068  rrhre  29393  erdszelem5  30431  wsuceq2  31006  taupilem1  32344  finxpreclem2  32403  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem27  32606  poimirlem30  32609  broucube  32613  mblfinlem1  32616  heiborlem6  32785  icccncfext  38773  dirkertrigeq  38994  zlmodzxzel  41926  dignn0flhalflem1  42207  onetansqsecsq  42301  cotsqcscsq  42302