Theorem mp3an 1277

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

Ref	Expression
mp3an.1	⊢ φ
mp3an.2	⊢ ψ
mp3an.3	⊢ χ
mp3an.4	⊢ ((φ ∧ ψ ∧ χ) → θ)

Assertion

Ref	Expression
mp3an	⊢ θ

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 ⊢ ψ
2		mp3an.3	. 2 ⊢ χ
3		mp3an.1	. . 3 ⊢ φ
4		mp3an.4	. . 3 ⊢ ((φ ∧ ψ ∧ χ) → θ)
5	3, 4	mp3an1 1264	. 2 ⊢ ((ψ ∧ χ) → θ)
6	1, 2, 5	mp2an 653	1 ⊢ θ

Syntax hints:   → wi 4   ∧ w3a 934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is referenced by:  vtocl3  2911  raltp  3781  rextp  3782  opkth  4132  otkelins2k  4255  otkelins3k  4256  caovass  5627  caovdi  5634  oprabid2  5646  clos1is  5881  clos10  5887  elmap  6017  elpm  6019  elpm2  6020  xpassen  6057  tcdi  6164  ce0addcnnul  6179  tlenc1c  6240  ncvsq  6256  nchoicelem9  6297  frecxp  6314