Theorem mp3an23 1224

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

Syntax hints:   → wi 4   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  sbciegf  2794  ac6sfi  6352  1qec  6486  ltaddnq  6505  halfnqq  6508  1idsr  6853  pn0sr  6856  muleqadd  7649  halfcl  8151  rehalfcl  8152  half0  8153  2halves  8154  halfpos2  8155  halfnneg2  8157  halfaddsub  8159  nneoor  8340  zeo  8343  fztp  8940  modqfrac  9179  imre  9451  reim  9452  crim  9458  addcj  9491  imval2  9494