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  2994  ac6sfi  6893  dju0en  7208  1qec  7382  ltaddnq  7401  halfnqq  7404  1idsr  7762  pn0sr  7765  ltm1sr  7771  muleqadd  8619  halfcl  9139  rehalfcl  9140  half0  9141  2halves  9142  halfpos2  9143  halfnneg2  9145  halfaddsub  9147  nneoor  9349  zeo  9352  fztp  10071  modqfrac  10330  iexpcyc  10617  bcn2  10735  bcpasc  10737  imre  10851  reim  10852  crim  10858  addcj  10891  imval2  10894  sinf  11703  efi4p  11716  resin4p  11717  recos4p  11718  sinneg  11725  efival  11731  cosadd  11736  sinmul  11743  sinbnd  11751  cosbnd  11752  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  sin01gt0  11760  cos01gt0  11761  sin02gt0  11762  odd2np1lem  11867  odd2np1  11868  pythagtriplem12  12265  pockthi  12346  mopnex  13787  sincosq1lem  14028  sincosq2sgn  14030  sincosq3sgn  14031  sincosq4sgn  14032  sinq12gt0  14033  abssinper  14049  coskpi  14051  rpcxpsqrt  14124  logsqrt  14125