Theorem mp3an23 1329

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  sbciegf  2995  ac6sfi  6898  dju0en  7213  1qec  7387  ltaddnq  7406  halfnqq  7409  1idsr  7767  pn0sr  7770  ltm1sr  7776  muleqadd  8625  halfcl  9145  rehalfcl  9146  half0  9147  2halves  9148  halfpos2  9149  halfnneg2  9151  halfaddsub  9153  nneoor  9355  zeo  9358  fztp  10078  modqfrac  10337  iexpcyc  10625  bcn2  10744  bcpasc  10746  imre  10860  reim  10861  crim  10867  addcj  10900  imval2  10903  sinf  11712  efi4p  11725  resin4p  11726  recos4p  11727  sinneg  11734  efival  11740  cosadd  11745  sinmul  11752  sinbnd  11760  cosbnd  11761  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  odd2np1lem  11877  odd2np1  11878  pythagtriplem12  12275  pockthi  12356  mopnex  14008  sincosq1lem  14249  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  abssinper  14270  coskpi  14272  rpcxpsqrt  14345  logsqrt  14346  2lgsoddprmlem2  14457