Theorem syl21anc 1270

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  4409  brcogw  4890  funprg  5370  funtpg  5371  fnunsn  5429  fun2d  5498  ftpg  5822  fsnunf  5838  isotr  5939  off  6229  caofrss  6248  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  pmresg  6821  ac6sfi  7056  tridc  7057  tpfidceq  7088  fidcenumlemrks  7116  sbthlemi8  7127  casefun  7248  caseinj  7252  djufun  7267  djuinj  7269  mulclpi  7511  archnqq  7600  addlocprlemlt  7714  addlocprlemeq  7716  addlocprlemgt  7717  mullocprlem  7753  apreim  8746  subrecap  8982  ltrec1  9031  divge0d  9929  fseq1p1m1  10286  q2submod  10602  seq3caopr2  10710  seqcaopr2g  10711  seq3distr  10749  facavg  10963  swrdwrdsymbg  11191  cats1un  11248  shftfibg  11326  sqrtdiv  11548  sqrtdivd  11674  mulcn2  11818  demoivreALT  12280  dvdslegcd  12480  gcdnncl  12483  qredeu  12614  rpdvds  12616  rpexp  12670  oddpwdclemodd  12689  divnumden  12713  divdenle  12714  phimullem  12742  phisum  12758  pythagtriplem4  12786  pythagtriplem8  12790  pythagtriplem9  12791  pcgcd1  12846  fldivp1  12866  pockthlem  12874  setsfun  13062  setsfun0  13063  strleund  13131  ercpbl  13359  sgrppropd  13441  mndpropd  13468  grpidssd  13604  grpinvssd  13605  issubg2m  13721  isnsg3  13739  eqgid  13758  kerf1ghm  13806  lmodprop2d  14306  lsspropdg  14389  znidomb  14616  znrrg  14618  comet  15167  fsumcncntop  15235  mulcncf  15276  mpodvdsmulf1o  15658  gausslemma2dlem0d  15725  gausslemma2dlem1a  15731  2lgslem1a1  15759  2sqlem8a  15795  2sqlem8  15796  trilpo  16370  neapmkv  16395