Theorem mp3an23 1340

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  sbciegf  3009  ac6sfi  6927  dju0en  7244  1qec  7418  ltaddnq  7437  halfnqq  7440  1idsr  7798  pn0sr  7801  ltm1sr  7807  muleqadd  8656  halfcl  9176  rehalfcl  9177  half0  9178  2halves  9179  halfpos2  9180  halfnneg2  9182  halfaddsub  9184  nneoor  9386  zeo  9389  fztp  10110  modqfrac  10370  iexpcyc  10659  bcn2  10779  bcpasc  10781  imre  10895  reim  10896  crim  10902  addcj  10935  imval2  10938  sinf  11747  efi4p  11760  resin4p  11761  recos4p  11762  sinneg  11769  efival  11775  cosadd  11780  sinmul  11787  sinbnd  11795  cosbnd  11796  ef01bndlem  11799  sin01bnd  11800  cos01bnd  11801  sin01gt0  11804  cos01gt0  11805  sin02gt0  11806  odd2np1lem  11912  odd2np1  11913  pythagtriplem12  12310  pockthi  12393  opprsubrngg  13575  isridl  13836  zlmval  13940  zlmlemg  13941  zlmsca  13945  zlmvscag  13946  mopnex  14482  sincosq1lem  14723  sincosq2sgn  14725  sincosq3sgn  14726  sincosq4sgn  14727  sinq12gt0  14728  abssinper  14744  coskpi  14746  rpcxpsqrt  14819  logsqrt  14820  2lgsoddprmlem2  14932