Theorem syl12anc 1276

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 )
syl12anc.4	|- ( ( ps /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
syl12anc	|- ( ph -> ta )

Proof of Theorem syl12anc

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	jca32 310	. 2 |- ( ph -> ( ps /\ ( ch /\ th ) ) )
5		syl12anc.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:  syl22anc  1279  cocan1  5996  fliftfun  6005  isopolem  6031  f1oiso2  6036  caovcld  6246  caovcomd  6249  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  1dom1el  7113  fidceq  7177  findcard2d  7201  diffifi  7204  tridc  7210  en2eqpr  7220  sbthlemi9  7289  supisolem  7354  ordiso2  7381  difinfsnlem  7445  difinfsn  7446  pr2cv1  7547  prarloclemup  7868  prarloc  7876  nqprl  7924  nqpru  7925  ltaddpr  7970  aptiprlemu  8013  archpr  8016  cauappcvgprlem2  8033  caucvgprlem2  8053  caucvgprprlem2  8083  suplocexprlemlub  8097  suplocexpr  8098  recexgt0sr  8146  archsr  8155  axpre-suploclemres  8274  conjmulap  9067  lerec2  9227  ledivp1  9241  cju  9299  nn2ge  9346  gtndiv  9751  supinfneg  10010  infsupneg  10011  z2ge  10244  iccssioo2  10364  fzrev3  10510  elfz1b  10513  zsupcllemstep  10678  zsupssdc  10689  exbtwnzlemstep  10698  exbtwnzlemex  10700  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnre  10707  flqdiv  10778  frec2uzled  10886  seq3caopr  10952  seqcaoprg  10953  iseqf1olemab  10959  iseqf1olemnanb  10960  seqf1oglem1  10976  expnegzap  11030  nn0ltexp2  11168  hashen  11244  hashunlem  11265  hashprg  11270  hashfibclem  11303  hashf1lem2  11307  leisorel  11310  zfz1isolemiso  11312  seq3coll  11315  swrdccat3b  11533  caucvgrelemrec  11766  resqrexlemex  11812  minmax  12019  xrminmax  12055  fsum2dlemstep  12225  fisumcom2  12229  zproddc  12370  fprod2dlemstep  12413  fprodcom2fi  12417  bezoutlemmain  12799  sqgcd  12830  pcpremul  13100  pceulem  13101  pceu  13102  pczpre  13104  pcdiv  13109  pcqmul  13110  pcqdiv  13114  pcexp  13116  pcdvdsb  13127  pcneg  13132  pcdvdstr  13134  pcgcd1  13135  pc2dvds  13137  pcz  13139  pcaddlem  13146  pcadd  13147  qexpz  13159  expnprm  13160  infpnlem2  13167  ballotfilemfc0  13289  ballotfilemfcc  13290  f1ocpbllem  13689  f1ovscpbl  13691  sgrppropd  13786  mndpropd  13811  grpsubpropd2  13968  f1ghm0to0  14133  ablnnncan  14216  rngpropd  14360  ringpropd  14449  lmodprop2d  14793  lsspropdg  14876  assapropd  15122  neiint  15388  restbasg  15411  iscnp4  15461  cnconst2  15476  cnpdis  15485  neitx  15511  upxp  15515  hmeoimaf1o  15557  blssexps  15672  blssex  15673  ssblex  15674  bdmopn  15747  xmettx  15753  metcnp3  15754  tgioo  15797  tgqioo  15798  dvmptfsum  15968  elply2  15978  sin0pilem2  16026  logbgcd1irr  16220  perfect  16318  bposlem2  16329  lgsval  16345  lgsfcl2  16347  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  clwwlknonex2e  16903  pwle2  17250  qdiff  17322