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  4410  brcogw  4891  funprg  5371  funtpg  5372  fnunsn  5430  fun2d  5501  ftpg  5827  fsnunf  5843  isotr  5946  off  6237  caofrss  6256  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  pmresg  6831  ac6sfi  7068  tridc  7070  eqsndc  7076  tpfidceq  7103  fidcenumlemrks  7131  sbthlemi8  7142  casefun  7263  caseinj  7267  djufun  7282  djuinj  7284  mulclpi  7526  archnqq  7615  addlocprlemlt  7729  addlocprlemeq  7731  addlocprlemgt  7732  mullocprlem  7768  apreim  8761  subrecap  8997  ltrec1  9046  divge0d  9945  fseq1p1m1  10302  q2submod  10619  seq3caopr2  10727  seqcaopr2g  10728  seq3distr  10766  facavg  10980  swrdwrdsymbg  11211  cats1un  11268  shftfibg  11346  sqrtdiv  11568  sqrtdivd  11694  mulcn2  11838  demoivreALT  12300  dvdslegcd  12500  gcdnncl  12503  qredeu  12634  rpdvds  12636  rpexp  12690  oddpwdclemodd  12709  divnumden  12733  divdenle  12734  phimullem  12762  phisum  12778  pythagtriplem4  12806  pythagtriplem8  12810  pythagtriplem9  12811  pcgcd1  12866  fldivp1  12886  pockthlem  12894  setsfun  13082  setsfun0  13083  strleund  13151  ercpbl  13379  sgrppropd  13461  mndpropd  13488  grpidssd  13624  grpinvssd  13625  issubg2m  13741  isnsg3  13759  eqgid  13778  kerf1ghm  13826  lmodprop2d  14327  lsspropdg  14410  znidomb  14637  znrrg  14639  comet  15188  fsumcncntop  15256  mulcncf  15297  mpodvdsmulf1o  15679  gausslemma2dlem0d  15746  gausslemma2dlem1a  15752  2lgslem1a1  15780  2sqlem8a  15816  2sqlem8  15817  trilpo  16471  neapmkv  16496