Theorem mp3an1 1264

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
mp3an1	|- ((ps /\ ch) -> th)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expb 1152	. 2 |- ((ph /\ (ps /\ ch)) -> th)
4	1, 3	mpan 651	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 358   /\ 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:  mp3an12  1267  mp3an1i  1270  mp3anl1  1271  mp3an  1277  opkelcokg  4262  opkelimagekg  4272  ltfintri  4467  vfinspnn  4542  vfinspclt  4553  spaccl  6287  spacind  6288  nchoicelem3  6292  nchoicelem4  6293  nchoicelem6  6295  nchoicelem9  6298  nchoicelem12  6301  nchoicelem14  6303  nchoicelem17  6306