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  3021  ac6sfi  6968  dju0en  7299  1qec  7474  ltaddnq  7493  halfnqq  7496  1idsr  7854  pn0sr  7857  ltm1sr  7863  muleqadd  8714  halfcl  9236  rehalfcl  9237  half0  9238  2halves  9239  halfpos2  9240  halfnneg2  9242  halfaddsub  9244  nneoor  9447  zeo  9450  fztp  10172  modqfrac  10448  iexpcyc  10755  bcn2  10875  bcpasc  10877  imre  11035  reim  11036  crim  11042  addcj  11075  imval2  11078  sinf  11888  efi4p  11901  resin4p  11902  recos4p  11903  sinneg  11910  efival  11916  cosadd  11921  sinmul  11928  sinbnd  11936  cosbnd  11937  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  odd2np1lem  12056  odd2np1  12057  pythagtriplem12  12471  pockthi  12554  opprsubrngg  13845  opprdomnbg  13908  isridl  14138  zlmval  14261  zlmlemg  14262  zlmsca  14266  zlmvscag  14267  mopnex  14849  sub1cncf  14946  sub2cncf  14947  sincosq1lem  15169  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  abssinper  15190  coskpi  15192  rpcxpsqrt  15266  logsqrt  15267  2lgsoddprmlem2  15455