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  4384  brcogw  4865  funprg  5343  funtpg  5344  fnunsn  5402  fun2d  5471  ftpg  5791  fsnunf  5807  isotr  5908  off  6194  caofrss  6213  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  pmresg  6786  ac6sfi  7021  tridc  7022  tpfidceq  7053  fidcenumlemrks  7081  sbthlemi8  7092  casefun  7213  caseinj  7217  djufun  7232  djuinj  7234  mulclpi  7476  archnqq  7565  addlocprlemlt  7679  addlocprlemeq  7681  addlocprlemgt  7682  mullocprlem  7718  apreim  8711  subrecap  8947  ltrec1  8996  divge0d  9894  fseq1p1m1  10251  q2submod  10567  seq3caopr2  10675  seqcaopr2g  10676  seq3distr  10714  facavg  10928  swrdwrdsymbg  11155  cats1un  11212  shftfibg  11246  sqrtdiv  11468  sqrtdivd  11594  mulcn2  11738  demoivreALT  12200  dvdslegcd  12400  gcdnncl  12403  qredeu  12534  rpdvds  12536  rpexp  12590  oddpwdclemodd  12609  divnumden  12633  divdenle  12634  phimullem  12662  phisum  12678  pythagtriplem4  12706  pythagtriplem8  12710  pythagtriplem9  12711  pcgcd1  12766  fldivp1  12786  pockthlem  12794  setsfun  12982  setsfun0  12983  strleund  13050  ercpbl  13278  sgrppropd  13360  mndpropd  13387  grpidssd  13523  grpinvssd  13524  issubg2m  13640  isnsg3  13658  eqgid  13677  kerf1ghm  13725  lmodprop2d  14225  lsspropdg  14308  znidomb  14535  znrrg  14537  comet  15086  fsumcncntop  15154  mulcncf  15195  mpodvdsmulf1o  15577  gausslemma2dlem0d  15644  gausslemma2dlem1a  15650  2lgslem1a1  15678  2sqlem8a  15714  2sqlem8  15715  trilpo  16184  neapmkv  16209