Theorem mp3an 1277

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

Hypotheses

Ref	Expression
mp3an.1	|- ph
mp3an.2	|- ps
mp3an.3	|- ch
mp3an.4	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ((ph /\ ps /\ ch) -> th)
5	3, 4	mp3an1 1264	. 2 |- ((ps /\ ch) -> th)
6	1, 2, 5	mp2an 653	1 |- th

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  2912  raltp  3782  rextp  3783  opkth  4133  otkelins2k  4256  otkelins3k  4257  caovass  5628  caovdi  5635  oprabid2  5647  clos1is  5882  clos10  5888  elmap  6018  elpm  6020  elpm2  6021  xpassen  6058  tcdi  6165  ce0addcnnul  6180  tlenc1c  6241  ncvsq  6257  nchoicelem9  6298  frecxp  6315