Theorem syl21anc 1232

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 307	. 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 103

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

This theorem is referenced by:  issod  4304  brcogw  4780  funprg  5248  funtpg  5249  fnunsn  5305  ftpg  5680  fsnunf  5696  isotr  5795  off  6073  caofrss  6085  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  pmresg  6654  ac6sfi  6876  tridc  6877  fidcenumlemrks  6930  sbthlemi8  6941  casefun  7062  caseinj  7066  djufun  7081  djuinj  7083  mulclpi  7290  archnqq  7379  addlocprlemlt  7493  addlocprlemeq  7495  addlocprlemgt  7496  mullocprlem  7532  apreim  8522  subrecap  8756  ltrec1  8804  divge0d  9694  fseq1p1m1  10050  q2submod  10341  seq3caopr2  10438  seq3distr  10469  facavg  10680  shftfibg  10784  sqrtdiv  11006  sqrtdivd  11132  mulcn2  11275  demoivreALT  11736  dvdslegcd  11919  gcdnncl  11922  qredeu  12051  rpdvds  12053  rpexp  12107  oddpwdclemodd  12126  divnumden  12150  divdenle  12151  phimullem  12179  phisum  12194  pythagtriplem4  12222  pythagtriplem8  12226  pythagtriplem9  12227  pcgcd1  12281  fldivp1  12300  pockthlem  12308  setsfun  12451  setsfun0  12452  strleund  12506  mndpropd  12676  comet  13293  fsumcncntop  13350  mulcncf  13385  2sqlem8a  13752  2sqlem8  13753  trilpo  14075  neapmkv  14099