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  6619  tfrcllembxssdm  6632  pmresg  6962  ac6sfi  7208  tridc  7210  eqsndc  7216  tpfidceq  7243  fidcenumlemrks  7277  sbthlemi8  7288  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  10154  fseq1p1m1  10517  q2submod  10842  seq3caopr2  10950  seqcaopr2g  10951  seq3distr  10989  facavg  11205  swrdwrdsymbg  11457  cats1un  11514  shftfibg  11606  sqrtdiv  11829  sqrtdivd  11956  mulcn2  12102  demoivreALT  12565  dvdslegcd  12765  gcdnncl  12768  qredeu  12899  rpdvds  12901  rpexp  12956  nnmaxpwlemnfac  12975  nnmaxpwlemparts  12976  divnumden  13000  divdenle  13001  phimullem  13031  phisum  13047  pythagtriplem4  13075  pythagtriplem8  13079  pythagtriplem9  13080  pcgcd1  13135  fldivp1  13155  pockthlem  13163  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfrcn0  13330  setsfun  13444  setsfun0  13445  strleund  13515  ercpbl  13710  sgrppropd  13786  mndpropd  13811  grpidssd  13939  grpinvssd  13940  issubg2m  14050  isnsg3  14068  eqgid  14087  kerf1ghm  14135  lmodprop2d  14793  lsspropdg  14876  znidomb  15101  znrrg  15103  comet  15742  fsumcncntop  15810  mulcncf  15851  zprmlogbaplem2  16233  birthdaylem3  16244  mpodvdsmulf1o  16301  gausslemma2dlem0d  16393  gausslemma2dlem1a  16399  2lgslem1a1  16427  2sqlem8a  16463  2sqlem8  16464  trilpo  17316  neapmkv  17342