Theorem syl21anc 1249

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 309	. 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 104

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

This theorem is referenced by:  issod  4366  brcogw  4847  funprg  5324  funtpg  5325  fnunsn  5383  ftpg  5768  fsnunf  5784  isotr  5885  off  6171  caofrss  6190  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  pmresg  6763  ac6sfi  6995  tridc  6996  tpfidceq  7027  fidcenumlemrks  7055  sbthlemi8  7066  casefun  7187  caseinj  7191  djufun  7206  djuinj  7208  mulclpi  7441  archnqq  7530  addlocprlemlt  7644  addlocprlemeq  7646  addlocprlemgt  7647  mullocprlem  7683  apreim  8676  subrecap  8912  ltrec1  8961  divge0d  9859  fseq1p1m1  10216  q2submod  10530  seq3caopr2  10638  seqcaopr2g  10639  seq3distr  10677  facavg  10891  swrdwrdsymbg  11117  shftfibg  11131  sqrtdiv  11353  sqrtdivd  11479  mulcn2  11623  demoivreALT  12085  dvdslegcd  12285  gcdnncl  12288  qredeu  12419  rpdvds  12421  rpexp  12475  oddpwdclemodd  12494  divnumden  12518  divdenle  12519  phimullem  12547  phisum  12563  pythagtriplem4  12591  pythagtriplem8  12595  pythagtriplem9  12596  pcgcd1  12651  fldivp1  12671  pockthlem  12679  setsfun  12867  setsfun0  12868  strleund  12935  ercpbl  13163  sgrppropd  13245  mndpropd  13272  grpidssd  13408  grpinvssd  13409  issubg2m  13525  isnsg3  13543  eqgid  13562  kerf1ghm  13610  lmodprop2d  14110  lsspropdg  14193  znidomb  14420  znrrg  14422  comet  14971  fsumcncntop  15039  mulcncf  15080  mpodvdsmulf1o  15462  gausslemma2dlem0d  15529  gausslemma2dlem1a  15535  2lgslem1a1  15563  2sqlem8a  15599  2sqlem8  15600  trilpo  15982  neapmkv  16007