Theorem mp3an23 1342

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  sbciegf  3034  ac6sfi  7010  dju0en  7342  1qec  7521  ltaddnq  7540  halfnqq  7543  1idsr  7901  pn0sr  7904  ltm1sr  7910  muleqadd  8761  halfcl  9283  rehalfcl  9284  half0  9285  2halves  9286  halfpos2  9287  halfnneg2  9289  halfaddsub  9291  nneoor  9495  zeo  9498  fztp  10220  modqfrac  10504  iexpcyc  10811  bcn2  10931  bcpasc  10933  imre  11237  reim  11238  crim  11244  addcj  11277  imval2  11280  sinf  12090  efi4p  12103  resin4p  12104  recos4p  12105  sinneg  12112  efival  12118  cosadd  12123  sinmul  12130  sinbnd  12138  cosbnd  12139  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  sin01gt0  12148  cos01gt0  12149  sin02gt0  12150  odd2np1lem  12258  odd2np1  12259  pythagtriplem12  12673  pockthi  12756  opprsubrngg  14048  opprdomnbg  14111  isridl  14341  zlmval  14464  zlmlemg  14465  zlmsca  14469  zlmvscag  14470  mopnex  15052  sub1cncf  15149  sub2cncf  15150  sincosq1lem  15372  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  sinq12gt0  15377  abssinper  15393  coskpi  15395  rpcxpsqrt  15469  logsqrt  15470  2lgsoddprmlem2  15658