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  5993  fliftfun  6002  isopolem  6028  f1oiso2  6033  caovcld  6243  caovcomd  6246  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  1dom1el  7107  fidceq  7171  findcard2d  7195  diffifi  7198  tridc  7204  en2eqpr  7214  sbthlemi9  7282  supisolem  7348  ordiso2  7375  difinfsnlem  7439  difinfsn  7440  pr2cv1  7541  prarloclemup  7862  prarloc  7870  nqprl  7918  nqpru  7919  ltaddpr  7964  aptiprlemu  8007  archpr  8010  cauappcvgprlem2  8027  caucvgprlem2  8047  caucvgprprlem2  8077  suplocexprlemlub  8091  suplocexpr  8092  recexgt0sr  8140  archsr  8149  axpre-suploclemres  8268  conjmulap  9061  lerec2  9221  ledivp1  9235  cju  9293  nn2ge  9339  gtndiv  9745  supinfneg  10004  infsupneg  10005  z2ge  10238  iccssioo2  10358  fzrev3  10504  elfz1b  10507  zsupcllemstep  10672  zsupssdc  10683  exbtwnzlemstep  10692  exbtwnzlemex  10694  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnre  10701  flqdiv  10771  frec2uzled  10879  seq3caopr  10945  seqcaoprg  10946  iseqf1olemab  10952  iseqf1olemnanb  10953  seqf1oglem1  10969  expnegzap  11023  nn0ltexp2  11161  hashen  11237  hashunlem  11258  hashprg  11263  hashfibclem  11296  hashf1lem2  11300  leisorel  11303  zfz1isolemiso  11305  seq3coll  11308  swrdccat3b  11526  caucvgrelemrec  11759  resqrexlemex  11805  minmax  12011  xrminmax  12047  fsum2dlemstep  12217  fisumcom2  12221  zproddc  12362  fprod2dlemstep  12405  fprodcom2fi  12409  bezoutlemmain  12791  sqgcd  12822  pcpremul  13092  pceulem  13093  pceu  13094  pczpre  13096  pcdiv  13101  pcqmul  13102  pcqdiv  13106  pcexp  13108  pcdvdsb  13119  pcneg  13124  pcdvdstr  13126  pcgcd1  13127  pc2dvds  13129  pcz  13131  pcaddlem  13138  pcadd  13139  qexpz  13151  expnprm  13152  infpnlem2  13159  ballotfilemfc0  13281  ballotfilemfcc  13282  f1ocpbllem  13680  f1ovscpbl  13682  sgrppropd  13777  mndpropd  13802  grpsubpropd2  13959  f1ghm0to0  14124  ablnnncan  14176  rngpropd  14303  ringpropd  14392  lmodprop2d  14734  lsspropdg  14817  assapropd  15063  neiint  15295  restbasg  15318  iscnp4  15368  cnconst2  15383  cnpdis  15392  neitx  15418  upxp  15422  hmeoimaf1o  15464  blssexps  15579  blssex  15580  ssblex  15581  bdmopn  15654  xmettx  15660  metcnp3  15661  tgioo  15704  tgqioo  15705  dvmptfsum  15875  elply2  15885  sin0pilem2  15933  logbgcd1irr  16122  perfect  16199  bposlem2  16210  lgsval  16221  lgsfcl2  16223  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  clwwlknonex2e  16779  pwle2  17126  qdiff  17196