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  7571  1qec  7756  ltaddnq  7775  halfnqq  7778  1idsr  8136  pn0sr  8139  ltm1sr  8145  muleqadd  9001  halfcl  9536  rehalfcl  9537  half0  9538  2halves  9539  halfpos2  9540  halfnneg2  9542  halfaddsub  9544  nneoor  9753  zeo  9756  fztp  10496  modqfrac  10789  iexpcyc  11096  bcn2  11218  bcpasc  11220  imre  11632  reim  11633  crim  11639  addcj  11672  imval2  11675  sinf  12490  efi4p  12503  resin4p  12504  recos4p  12505  sinneg  12512  efival  12518  cosadd  12523  sinmul  12530  sinbnd  12538  cosbnd  12539  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  odd2np1lem  12658  odd2np1  12659  pythagtriplem12  13077  pockthi  13160  prmlem0  13243  opprsubrngg  14603  opprdomnbg  14667  isridl  14925  zlmval  15046  zlmlemg  15047  zlmsca  15051  zlmvscag  15052  mopnex  15697  sub1cncf  15794  sub2cncf  15795  sincosq1lem  16018  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  abssinper  16039  coskpi  16041  rpcxpsqrt  16119  logsqrt  16120  ppiqub  16254  chtublem  16256  chtqub  16257  bcmax  16266  bcp1ctr  16267  bposlem2  16273  bposlem6  16277  bposlem9  16280  2lgsoddprmlem2  16391