Theorem mp3an23 1365

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

Syntax hints:   → wi 4   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  sbciegf  3063  ac6sfi  7087  dju0en  7429  1qec  7608  ltaddnq  7627  halfnqq  7630  1idsr  7988  pn0sr  7991  ltm1sr  7997  muleqadd  8848  halfcl  9370  rehalfcl  9371  half0  9372  2halves  9373  halfpos2  9374  halfnneg2  9376  halfaddsub  9378  nneoor  9582  zeo  9585  fztp  10313  modqfrac  10600  iexpcyc  10907  bcn2  11027  bcpasc  11029  imre  11429  reim  11430  crim  11436  addcj  11469  imval2  11472  sinf  12283  efi4p  12296  resin4p  12297  recos4p  12298  sinneg  12305  efival  12311  cosadd  12316  sinmul  12323  sinbnd  12331  cosbnd  12332  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  odd2np1lem  12451  odd2np1  12452  pythagtriplem12  12866  pockthi  12949  opprsubrngg  14244  opprdomnbg  14307  isridl  14537  zlmval  14660  zlmlemg  14661  zlmsca  14665  zlmvscag  14666  mopnex  15248  sub1cncf  15345  sub2cncf  15346  sincosq1lem  15568  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  abssinper  15589  coskpi  15591  rpcxpsqrt  15665  logsqrt  15666  2lgsoddprmlem2  15854