Theorem syl21anc 1134

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

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

Assertion

Ref	Expression
syl21anc	|- ( ph -> ta )

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 292	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		syl21anc.4	. 2 |- ( ( ( ps /\ ch ) /\ th ) -> ta )
6	4, 5	syl 14	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  issod  4056  brcogw  4504  funprg  4949  funtpg  4950  fnunsn  5006  ftpg  5347  fsnunf  5362  isotr  5456  off  5724  caofrss  5735  ac6sfi  6352  mulclpi  6426  archnqq  6515  addlocprlemlt  6629  addlocprlemeq  6631  addlocprlemgt  6632  mullocprlem  6668  apreim  7594  ltrec1  7854  divge0d  8663  fseq1p1m1  8956  iseqcaopr2  9241  iseqdistr  9249  shftfibg  9421  sqrtdiv  9640  sqrtdivd  9764  mulcn2  9833