Theorem mp3an23 1288

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

Syntax hints:   → wi 4   ∧ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  sbciegf  2906  ac6sfi  6743  dju0en  7015  1qec  7138  ltaddnq  7157  halfnqq  7160  1idsr  7505  pn0sr  7508  muleqadd  8336  halfcl  8844  rehalfcl  8845  half0  8846  2halves  8847  halfpos2  8848  halfnneg2  8850  halfaddsub  8852  nneoor  9051  zeo  9054  fztp  9745  modqfrac  9997  iexpcyc  10284  bcn2  10397  bcpasc  10399  imre  10510  reim  10511  crim  10517  addcj  10550  imval2  10553  sinf  11256  efi4p  11269  resin4p  11270  recos4p  11271  sinneg  11278  efival  11284  cosadd  11289  sinmul  11296  sinbnd  11304  cosbnd  11305  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  sin01gt0  11313  cos01gt0  11314  sin02gt0  11315  odd2np1lem  11411  odd2np1  11412  mopnex  12488