Theorem syl21anc 1169

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 302	. 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 102

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

This theorem is referenced by:  issod  4082  brcogw  4532  funprg  4980  funtpg  4981  fnunsn  5037  ftpg  5379  fsnunf  5394  isotr  5487  off  5755  caofrss  5766  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  ac6sfi  6431  mulclpi  6580  archnqq  6669  addlocprlemlt  6783  addlocprlemeq  6785  addlocprlemgt  6786  mullocprlem  6822  apreim  7770  ltrec1  8033  divge0d  8895  fseq1p1m1  9187  q2submod  9467  iseqoveq  9540  iseqcaopr2  9557  iseqdistr  9567  facavg  9770  shftfibg  9846  sqrtdiv  10066  sqrtdivd  10192  mulcn2  10289  dvdslegcd  10500  gcdnncl  10503  qredeu  10623  rpdvds  10625  rpexp  10676  oddpwdclemodd  10694