Theorem syl21anc 1277

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  4459  brcogw  4944  funprg  5426  funtpg  5427  fnunsn  5485  fun2d  5558  ftpg  5890  fsnunf  5906  isotr  6012  off  6305  caofrss  6324  suppssfvg  6493  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  pmresg  6947  ac6sfi  7192  tridc  7194  eqsndc  7200  tpfidceq  7227  fidcenumlemrks  7260  sbthlemi8  7271  casefun  7415  caseinj  7419  djufun  7434  djuinj  7436  mulclpi  7685  archnqq  7774  addlocprlemlt  7888  addlocprlemeq  7890  addlocprlemgt  7891  mullocprlem  7927  apreim  8921  subrecap  9159  ltrec1  9208  divge0d  10117  fseq1p1m1  10479  q2submod  10800  seq3caopr2  10908  seqcaopr2g  10909  seq3distr  10947  facavg  11162  swrdwrdsymbg  11414  cats1un  11471  shftfibg  11563  sqrtdiv  11786  sqrtdivd  11912  mulcn2  12056  demoivreALT  12519  dvdslegcd  12719  gcdnncl  12722  qredeu  12853  rpdvds  12855  rpexp  12909  oddpwdclemodd  12928  divnumden  12952  divdenle  12953  phimullem  12981  phisum  12997  pythagtriplem4  13025  pythagtriplem8  13029  pythagtriplem9  13030  pcgcd1  13085  fldivp1  13105  pockthlem  13113  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfrcn0  13251  setsfun  13365  setsfun0  13366  strleund  13434  ercpbl  13629  sgrppropd  13705  mndpropd  13730  grpidssd  13858  grpinvssd  13859  issubg2m  13969  isnsg3  13987  eqgid  14006  kerf1ghm  14054  lmodprop2d  14657  lsspropdg  14740  znidomb  14965  znrrg  14967  comet  15523  fsumcncntop  15591  mulcncf  15632  mpodvdsmulf1o  16018  gausslemma2dlem0d  16085  gausslemma2dlem1a  16091  2lgslem1a1  16119  2sqlem8a  16155  2sqlem8  16156  trilpo  16997  neapmkv  17023