Theorem mp3an23 1319

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 1316	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 422	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  sbciegf  2982  ac6sfi  6864  dju0en  7170  1qec  7329  ltaddnq  7348  halfnqq  7351  1idsr  7709  pn0sr  7712  ltm1sr  7718  muleqadd  8565  halfcl  9083  rehalfcl  9084  half0  9085  2halves  9086  halfpos2  9087  halfnneg2  9089  halfaddsub  9091  nneoor  9293  zeo  9296  fztp  10013  modqfrac  10272  iexpcyc  10559  bcn2  10677  bcpasc  10679  imre  10793  reim  10794  crim  10800  addcj  10833  imval2  10836  sinf  11645  efi4p  11658  resin4p  11659  recos4p  11660  sinneg  11667  efival  11673  cosadd  11678  sinmul  11685  sinbnd  11693  cosbnd  11694  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  odd2np1lem  11809  odd2np1  11810  pythagtriplem12  12207  pockthi  12288  mopnex  13155  sincosq1lem  13396  sincosq2sgn  13398  sincosq3sgn  13399  sincosq4sgn  13400  sinq12gt0  13401  abssinper  13417  coskpi  13419  rpcxpsqrt  13492  logsqrt  13493