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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  syl22anc  1279  cocan1  5983  fliftfun  5992  isopolem  6018  f1oiso2  6023  caovcld  6233  caovcomd  6236  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  1dom1el  7097  fidceq  7161  findcard2d  7185  diffifi  7188  tridc  7194  en2eqpr  7204  sbthlemi9  7272  supisolem  7338  ordiso2  7365  difinfsnlem  7429  difinfsn  7430  pr2cv1  7531  prarloclemup  7852  prarloc  7860  nqprl  7908  nqpru  7909  ltaddpr  7954  aptiprlemu  7997  archpr  8000  cauappcvgprlem2  8017  caucvgprlem2  8037  caucvgprprlem2  8067  suplocexprlemlub  8081  suplocexpr  8082  recexgt0sr  8130  archsr  8139  axpre-suploclemres  8258  conjmulap  9049  lerec2  9209  ledivp1  9223  cju  9281  nn2ge  9316  gtndiv  9720  supinfneg  9974  infsupneg  9975  z2ge  10207  iccssioo2  10327  fzrev3  10472  elfz1b  10475  zsupcllemstep  10640  zsupssdc  10651  exbtwnzlemstep  10660  exbtwnzlemex  10662  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnre  10669  flqdiv  10736  frec2uzled  10844  seq3caopr  10910  seqcaoprg  10911  iseqf1olemab  10917  iseqf1olemnanb  10918  seqf1oglem1  10934  expnegzap  10988  nn0ltexp2  11125  hashen  11201  hashunlem  11222  hashprg  11227  hashfibclem  11260  hashf1lem2  11264  leisorel  11267  zfz1isolemiso  11269  seq3coll  11272  swrdccat3b  11490  caucvgrelemrec  11723  resqrexlemex  11769  minmax  11974  xrminmax  12009  fsum2dlemstep  12179  fisumcom2  12183  zproddc  12324  fprod2dlemstep  12367  fprodcom2fi  12371  bezoutlemmain  12753  sqgcd  12784  pcpremul  13050  pceulem  13051  pceu  13052  pczpre  13054  pcdiv  13059  pcqmul  13060  pcqdiv  13064  pcexp  13066  pcdvdsb  13077  pcneg  13082  pcdvdstr  13084  pcgcd1  13085  pc2dvds  13087  pcz  13089  pcaddlem  13096  pcadd  13097  qexpz  13109  expnprm  13110  infpnlem2  13117  ballotfilemfc0  13210  ballotfilemfcc  13211  f1ocpbllem  13608  f1ovscpbl  13610  sgrppropd  13705  mndpropd  13730  grpsubpropd2  13887  f1ghm0to0  14052  ablnnncan  14104  rngpropd  14229  ringpropd  14316  lmodprop2d  14657  lsspropdg  14740  neiint  15169  restbasg  15192  iscnp4  15242  cnconst2  15257  cnpdis  15266  neitx  15292  upxp  15296  hmeoimaf1o  15338  blssexps  15453  blssex  15454  ssblex  15455  bdmopn  15528  xmettx  15534  metcnp3  15535  tgioo  15578  tgqioo  15579  dvmptfsum  15749  elply2  15759  sin0pilem2  15806  logbgcd1irr  15992  perfect  16029  lgsval  16037  lgsfcl2  16039  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  clwwlknonex2e  16595  pwle2  16942  qdiff  17003