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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  issod  4464  brcogw  4949  funprg  5431  funtpg  5432  fnunsn  5490  fun2d  5563  ftpg  5899  fsnunf  5915  isotr  6022  off  6315  caofrss  6334  suppssfvg  6503  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  pmresg  6957  ac6sfi  7202  tridc  7204  eqsndc  7210  tpfidceq  7237  fidcenumlemrks  7270  sbthlemi8  7281  casefun  7425  caseinj  7429  djufun  7444  djuinj  7446  mulclpi  7695  archnqq  7784  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  mullocprlem  7937  apreim  8931  subrecap  9169  ltrec1  9218  divge0d  10138  fseq1p1m1  10501  q2submod  10822  seq3caopr2  10930  seqcaopr2g  10931  seq3distr  10969  facavg  11184  swrdwrdsymbg  11436  cats1un  11493  shftfibg  11585  sqrtdiv  11808  sqrtdivd  11934  mulcn2  12078  demoivreALT  12541  dvdslegcd  12741  gcdnncl  12744  qredeu  12875  rpdvds  12877  rpexp  12931  oddpwdclemodd  12950  divnumden  12974  divdenle  12975  phimullem  13003  phisum  13019  pythagtriplem4  13047  pythagtriplem8  13051  pythagtriplem9  13052  pcgcd1  13107  fldivp1  13127  pockthlem  13135  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfrcn0  13273  setsfun  13387  setsfun0  13388  strleund  13457  ercpbl  13652  sgrppropd  13728  mndpropd  13753  grpidssd  13881  grpinvssd  13882  issubg2m  13992  isnsg3  14010  eqgid  14029  kerf1ghm  14077  lmodprop2d  14685  lsspropdg  14768  znidomb  14993  znrrg  14995  comet  15600  fsumcncntop  15668  mulcncf  15709  birthdaylem3  16089  mpodvdsmulf1o  16104  gausslemma2dlem0d  16171  gausslemma2dlem1a  16177  2lgslem1a1  16205  2sqlem8a  16241  2sqlem8  16242  trilpo  17092  neapmkv  17118