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  4466  brcogw  4951  funprg  5434  funtpg  5435  fnunsn  5493  fun2d  5566  ftpg  5902  fsnunf  5918  isotr  6025  off  6319  caofrss  6338  suppssfvg  6507  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  pmresg  6961  ac6sfi  7206  tridc  7208  eqsndc  7214  tpfidceq  7241  fidcenumlemrks  7275  sbthlemi8  7286  casefun  7431  caseinj  7435  djufun  7450  djuinj  7452  mulclpi  7701  archnqq  7790  addlocprlemlt  7904  addlocprlemeq  7906  addlocprlemgt  7907  mullocprlem  7943  apreim  8939  subrecap  9177  ltrec1  9226  divge0d  10155  fseq1p1m1  10518  q2submod  10843  seq3caopr2  10951  seqcaopr2g  10952  seq3distr  10990  facavg  11206  swrdwrdsymbg  11458  cats1un  11515  shftfibg  11607  sqrtdiv  11830  sqrtdivd  11957  mulcn2  12103  demoivreALT  12566  dvdslegcd  12766  gcdnncl  12769  qredeu  12900  rpdvds  12902  rpexp  12957  nnmaxpwlemnfac  12976  nnmaxpwlemparts  12977  divnumden  13001  divdenle  13002  phimullem  13032  phisum  13048  pythagtriplem4  13076  pythagtriplem8  13080  pythagtriplem9  13081  pcgcd1  13136  fldivp1  13156  pockthlem  13164  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfrcn0  13331  setsfun  13445  setsfun0  13446  strleund  13516  ercpbl  13711  sgrppropd  13787  mndpropd  13812  grpidssd  13940  grpinvssd  13941  issubg2m  14051  isnsg3  14069  eqgid  14088  kerf1ghm  14136  lmodprop2d  14794  lsspropdg  14877  znidomb  15102  znrrg  15104  comet  15725  fsumcncntop  15793  mulcncf  15834  zprmlogbaplem2  16216  birthdaylem3  16227  mpodvdsmulf1o  16284  gausslemma2dlem0d  16376  gausslemma2dlem1a  16382  2lgslem1a1  16410  2sqlem8a  16446  2sqlem8  16447  trilpo  17299  neapmkv  17325