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  4414  brcogw  4897  funprg  5377  funtpg  5378  fnunsn  5436  fun2d  5507  ftpg  5833  fsnunf  5849  isotr  5952  off  6243  caofrss  6262  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  pmresg  6840  ac6sfi  7080  tridc  7082  eqsndc  7088  tpfidceq  7115  fidcenumlemrks  7143  sbthlemi8  7154  casefun  7275  caseinj  7279  djufun  7294  djuinj  7296  mulclpi  7538  archnqq  7627  addlocprlemlt  7741  addlocprlemeq  7743  addlocprlemgt  7744  mullocprlem  7780  apreim  8773  subrecap  9009  ltrec1  9058  divge0d  9962  fseq1p1m1  10319  q2submod  10637  seq3caopr2  10745  seqcaopr2g  10746  seq3distr  10784  facavg  10998  swrdwrdsymbg  11235  cats1un  11292  shftfibg  11371  sqrtdiv  11593  sqrtdivd  11719  mulcn2  11863  demoivreALT  12325  dvdslegcd  12525  gcdnncl  12528  qredeu  12659  rpdvds  12661  rpexp  12715  oddpwdclemodd  12734  divnumden  12758  divdenle  12759  phimullem  12787  phisum  12803  pythagtriplem4  12831  pythagtriplem8  12835  pythagtriplem9  12836  pcgcd1  12891  fldivp1  12911  pockthlem  12919  setsfun  13107  setsfun0  13108  strleund  13176  ercpbl  13404  sgrppropd  13486  mndpropd  13513  grpidssd  13649  grpinvssd  13650  issubg2m  13766  isnsg3  13784  eqgid  13803  kerf1ghm  13851  lmodprop2d  14352  lsspropdg  14435  znidomb  14662  znrrg  14664  comet  15213  fsumcncntop  15281  mulcncf  15322  mpodvdsmulf1o  15704  gausslemma2dlem0d  15771  gausslemma2dlem1a  15777  2lgslem1a1  15805  2sqlem8a  15841  2sqlem8  15842  trilpo  16583  neapmkv  16608