Theorem syl21anc 1248

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  4365  brcogw  4846  funprg  5323  funtpg  5324  fnunsn  5382  ftpg  5767  fsnunf  5783  isotr  5884  off  6170  caofrss  6189  tfr1onlembxssdm  6428  tfrcllembxssdm  6441  pmresg  6762  ac6sfi  6994  tridc  6995  tpfidceq  7026  fidcenumlemrks  7054  sbthlemi8  7065  casefun  7186  caseinj  7190  djufun  7205  djuinj  7207  mulclpi  7440  archnqq  7529  addlocprlemlt  7643  addlocprlemeq  7645  addlocprlemgt  7646  mullocprlem  7682  apreim  8675  subrecap  8911  ltrec1  8960  divge0d  9858  fseq1p1m1  10215  q2submod  10528  seq3caopr2  10636  seqcaopr2g  10637  seq3distr  10675  facavg  10889  shftfibg  11102  sqrtdiv  11324  sqrtdivd  11450  mulcn2  11594  demoivreALT  12056  dvdslegcd  12256  gcdnncl  12259  qredeu  12390  rpdvds  12392  rpexp  12446  oddpwdclemodd  12465  divnumden  12489  divdenle  12490  phimullem  12518  phisum  12534  pythagtriplem4  12562  pythagtriplem8  12566  pythagtriplem9  12567  pcgcd1  12622  fldivp1  12642  pockthlem  12650  setsfun  12838  setsfun0  12839  strleund  12906  ercpbl  13134  sgrppropd  13216  mndpropd  13243  grpidssd  13379  grpinvssd  13380  issubg2m  13496  isnsg3  13514  eqgid  13533  kerf1ghm  13581  lmodprop2d  14081  lsspropdg  14164  znidomb  14391  znrrg  14393  comet  14942  fsumcncntop  15010  mulcncf  15051  mpodvdsmulf1o  15433  gausslemma2dlem0d  15500  gausslemma2dlem1a  15506  2lgslem1a1  15534  2sqlem8a  15570  2sqlem8  15571  trilpo  15944  neapmkv  15969