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  7426  caseinj  7430  djufun  7445  djuinj  7447  mulclpi  7696  archnqq  7785  addlocprlemlt  7899  addlocprlemeq  7901  addlocprlemgt  7902  mullocprlem  7938  apreim  8934  subrecap  9172  ltrec1  9221  divge0d  10149  fseq1p1m1  10512  q2submod  10837  seq3caopr2  10945  seqcaopr2g  10946  seq3distr  10984  facavg  11200  swrdwrdsymbg  11452  cats1un  11509  shftfibg  11601  sqrtdiv  11824  sqrtdivd  11951  mulcn2  12097  demoivreALT  12560  dvdslegcd  12760  gcdnncl  12763  qredeu  12894  rpdvds  12896  rpexp  12951  nnmaxpwlemnfac  12970  nnmaxpwlemparts  12971  divnumden  12995  divdenle  12996  phimullem  13026  phisum  13042  pythagtriplem4  13070  pythagtriplem8  13074  pythagtriplem9  13075  pcgcd1  13130  fldivp1  13150  pockthlem  13158  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfrcn0  13325  setsfun  13439  setsfun0  13440  strleund  13510  ercpbl  13705  sgrppropd  13781  mndpropd  13806  grpidssd  13934  grpinvssd  13935  issubg2m  14045  isnsg3  14063  eqgid  14082  kerf1ghm  14130  lmodprop2d  14769  lsspropdg  14852  znidomb  15077  znrrg  15079  comet  15691  fsumcncntop  15759  mulcncf  15800  zprmlogbaplem2  16177  birthdaylem3  16188  mpodvdsmulf1o  16245  gausslemma2dlem0d  16337  gausslemma2dlem1a  16343  2lgslem1a1  16371  2sqlem8a  16407  2sqlem8  16408  trilpo  17259  neapmkv  17285