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  8933  subrecap  9171  ltrec1  9220  divge0d  10148  fseq1p1m1  10511  q2submod  10835  seq3caopr2  10943  seqcaopr2g  10944  seq3distr  10982  facavg  11198  swrdwrdsymbg  11450  cats1un  11507  shftfibg  11599  sqrtdiv  11822  sqrtdivd  11949  mulcn2  12094  demoivreALT  12557  dvdslegcd  12757  gcdnncl  12760  qredeu  12891  rpdvds  12893  rpexp  12948  nnmaxpwlemnfac  12967  nnmaxpwlemparts  12968  divnumden  12992  divdenle  12993  phimullem  13023  phisum  13039  pythagtriplem4  13067  pythagtriplem8  13071  pythagtriplem9  13072  pcgcd1  13127  fldivp1  13147  pockthlem  13155  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfrcn0  13322  setsfun  13436  setsfun0  13437  strleund  13506  ercpbl  13701  sgrppropd  13777  mndpropd  13802  grpidssd  13930  grpinvssd  13931  issubg2m  14041  isnsg3  14059  eqgid  14078  kerf1ghm  14126  lmodprop2d  14734  lsspropdg  14817  znidomb  15042  znrrg  15044  comet  15649  fsumcncntop  15717  mulcncf  15758  zprmlogbaplem2  16135  birthdaylem3  16146  mpodvdsmulf1o  16185  gausslemma2dlem0d  16269  gausslemma2dlem1a  16275  2lgslem1a1  16303  2sqlem8a  16339  2sqlem8  16340  trilpo  17190  neapmkv  17216