Theorem mp3an23 1261

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

Syntax hints:   → wi 4   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  sbciegf  2856  ac6sfi  6544  1qec  6850  ltaddnq  6869  halfnqq  6872  1idsr  7217  pn0sr  7220  muleqadd  8035  halfcl  8534  rehalfcl  8535  half0  8536  2halves  8537  halfpos2  8538  halfnneg2  8540  halfaddsub  8542  nneoor  8744  zeo  8747  fztp  9385  modqfrac  9633  iexpcyc  9895  bcn2  10007  bcpasc  10009  imre  10112  reim  10113  crim  10119  addcj  10152  imval2  10155  odd2np1lem  10652  odd2np1  10653