Theorem mp3an23 1370

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1367	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 429	1 ⊢ (𝜑 → 𝜃)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  sbciegf  3083  ac6sfi  7202  dju0en  7570  1qec  7755  ltaddnq  7774  halfnqq  7777  1idsr  8135  pn0sr  8138  ltm1sr  8144  muleqadd  8998  halfcl  9531  rehalfcl  9532  half0  9533  2halves  9534  halfpos2  9535  halfnneg2  9537  halfaddsub  9539  nneoor  9748  zeo  9751  fztp  10485  modqfrac  10774  iexpcyc  11081  bcn2  11202  bcpasc  11204  imre  11616  reim  11617  crim  11623  addcj  11656  imval2  11659  sinf  12471  efi4p  12484  resin4p  12485  recos4p  12486  sinneg  12493  efival  12499  cosadd  12504  sinmul  12511  sinbnd  12519  cosbnd  12520  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  odd2np1lem  12639  odd2np1  12640  pythagtriplem12  13054  pockthi  13137  opprsubrngg  14519  opprdomnbg  14583  isridl  14841  zlmval  14962  zlmlemg  14963  zlmsca  14967  zlmvscag  14968  mopnex  15606  sub1cncf  15703  sub2cncf  15704  sincosq1lem  15926  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  abssinper  15947  coskpi  15949  rpcxpsqrt  16024  logsqrt  16025  2lgsoddprmlem2  16225