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  6600  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  1dom1el  7111  fidceq  7175  findcard2d  7199  diffifi  7202  tridc  7208  en2eqpr  7218  sbthlemi9  7287  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  9752  supinfneg  10011  infsupneg  10012  z2ge  10245  iccssioo2  10365  fzrev3  10511  elfz1b  10514  zsupcllemstep  10679  zsupssdc  10690  exbtwnzlemstep  10699  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnre  10708  flqdiv  10779  frec2uzled  10887  seq3caopr  10953  seqcaoprg  10954  iseqf1olemab  10960  iseqf1olemnanb  10961  seqf1oglem1  10977  expnegzap  11031  nn0ltexp2  11169  hashen  11245  hashunlem  11266  hashprg  11271  hashfibclem  11304  hashf1lem2  11308  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  swrdccat3b  11534  caucvgrelemrec  11767  resqrexlemex  11813  minmax  12020  xrminmax  12056  fsum2dlemstep  12226  fisumcom2  12230  zproddc  12371  fprod2dlemstep  12414  fprodcom2fi  12418  bezoutlemmain  12800  sqgcd  12831  pcpremul  13101  pceulem  13102  pceu  13103  pczpre  13105  pcdiv  13110  pcqmul  13111  pcqdiv  13115  pcexp  13117  pcdvdsb  13128  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pc2dvds  13138  pcz  13140  pcaddlem  13147  pcadd  13148  qexpz  13160  expnprm  13161  infpnlem2  13168  ballotfilemfc0  13290  ballotfilemfcc  13291  f1ocpbllem  13690  f1ovscpbl  13692  sgrppropd  13787  mndpropd  13812  grpsubpropd2  13969  f1ghm0to0  14134  ablnnncan  14217  rngpropd  14361  ringpropd  14450  lmodprop2d  14794  lsspropdg  14877  assapropd  15123  neiint  15371  restbasg  15394  iscnp4  15444  cnconst2  15459  cnpdis  15468  neitx  15494  upxp  15498  hmeoimaf1o  15540  blssexps  15655  blssex  15656  ssblex  15657  bdmopn  15730  xmettx  15736  metcnp3  15737  tgioo  15780  tgqioo  15781  dvmptfsum  15951  elply2  15961  sin0pilem2  16009  logbgcd1irr  16203  perfect  16301  bposlem2  16312  lgsval  16328  lgsfcl2  16330  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  clwwlknonex2e  16886  pwle2  17233  qdiff  17305