Theorem mp3an12i 1428

Description: mp3an 1424 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

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

Assertion

Ref	Expression
mp3an12i	|- ( ch -> ta )

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 |- ( ch -> th )
2		mp3an12i.1	. . 3 |- ph
3		mp3an12i.2	. . 3 |- ps
4		mp3an12i.4	. . 3 |- ( ( ph /\ ps /\ th ) -> ta )
5	2, 3, 4	mp3an12 1414	. 2 |- ( th -> ta )
6	1, 5	syl 17	1 |- ( ch -> ta )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ener  8002  hashfun  13224  funcnvs2  13658  3dvds  15052  oddp1d2  15082  bitsres  15195  bposlem9  25017  gausslemma2dlem1  25091  umgr2v2e  26421  0wlkonlem2  26980  eulerpartlemgvv  30438  scutbdaybnd  31921  scutbdaylt  31922  poimirlem26  33435  mblfinlem2  33447  isosctrlem1ALT  39170  fmtnorec1  41449  evengpoap3  41687