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  7206  dju0en  7576  1qec  7761  ltaddnq  7780  halfnqq  7783  1idsr  8141  pn0sr  8144  ltm1sr  8150  muleqadd  9006  halfcl  9542  rehalfcl  9543  half0  9544  2halves  9545  halfpos2  9546  halfnneg2  9548  halfaddsub  9550  nneoor  9759  zeo  9762  fztp  10502  modqfrac  10795  iexpcyc  11102  bcn2  11224  bcpasc  11226  imre  11638  reim  11639  crim  11645  addcj  11678  imval2  11681  sinf  12496  efi4p  12509  resin4p  12510  recos4p  12511  sinneg  12518  efival  12524  cosadd  12529  sinmul  12536  sinbnd  12544  cosbnd  12545  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  odd2np1lem  12664  odd2np1  12665  pythagtriplem12  13083  pockthi  13166  prmlem0  13249  opprsubrngg  14628  opprdomnbg  14692  isridl  14950  zlmval  15071  zlmlemg  15072  zlmsca  15076  zlmvscag  15077  mopnex  15731  sub1cncf  15828  sub2cncf  15829  sincosq1lem  16052  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  abssinper  16073  coskpi  16075  sineq0re  16076  rpcxpsqrt  16157  logsqrt  16158  ppiqub  16293  chtublem  16295  chtqub  16296  bcmax  16305  bcp1ctr  16306  bposlem2  16312  bposlem6  16316  bposlem9  16319  2lgsoddprmlem2  16430