Theorem mp3an23 1342

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  sbciegf  3030  ac6sfi  6997  dju0en  7328  1qec  7503  ltaddnq  7522  halfnqq  7525  1idsr  7883  pn0sr  7886  ltm1sr  7892  muleqadd  8743  halfcl  9265  rehalfcl  9266  half0  9267  2halves  9268  halfpos2  9269  halfnneg2  9271  halfaddsub  9273  nneoor  9477  zeo  9480  fztp  10202  modqfrac  10484  iexpcyc  10791  bcn2  10911  bcpasc  10913  imre  11195  reim  11196  crim  11202  addcj  11235  imval2  11238  sinf  12048  efi4p  12061  resin4p  12062  recos4p  12063  sinneg  12070  efival  12076  cosadd  12081  sinmul  12088  sinbnd  12096  cosbnd  12097  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  sin01gt0  12106  cos01gt0  12107  sin02gt0  12108  odd2np1lem  12216  odd2np1  12217  pythagtriplem12  12631  pockthi  12714  opprsubrngg  14006  opprdomnbg  14069  isridl  14299  zlmval  14422  zlmlemg  14423  zlmsca  14427  zlmvscag  14428  mopnex  15010  sub1cncf  15107  sub2cncf  15108  sincosq1lem  15330  sincosq2sgn  15332  sincosq3sgn  15333  sincosq4sgn  15334  sinq12gt0  15335  abssinper  15351  coskpi  15353  rpcxpsqrt  15427  logsqrt  15428  2lgsoddprmlem2  15616