Theorem syl12anc 1269

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  1272  cocan1  5910  fliftfun  5919  isopolem  5945  f1oiso2  5950  caovcld  6158  caovcomd  6161  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  fidceq  7027  findcard2d  7049  diffifi  7052  tridc  7057  en2eqpr  7065  sbthlemi9  7128  supisolem  7171  ordiso2  7198  difinfsnlem  7262  difinfsn  7263  pr2cv1  7364  prarloclemup  7678  prarloc  7686  nqprl  7734  nqpru  7735  ltaddpr  7780  aptiprlemu  7823  archpr  7826  cauappcvgprlem2  7843  caucvgprlem2  7863  caucvgprprlem2  7893  suplocexprlemlub  7907  suplocexpr  7908  recexgt0sr  7956  archsr  7965  axpre-suploclemres  8084  conjmulap  8872  lerec2  9032  ledivp1  9046  cju  9104  nn2ge  9139  gtndiv  9538  supinfneg  9786  infsupneg  9787  z2ge  10018  iccssioo2  10138  fzrev3  10279  elfz1b  10282  zsupcllemstep  10444  zsupssdc  10453  exbtwnzlemstep  10462  exbtwnzlemex  10464  rebtwn2zlemstep  10467  rebtwn2z  10469  qbtwnre  10471  flqdiv  10538  frec2uzled  10646  seq3caopr  10712  seqcaoprg  10713  iseqf1olemab  10719  iseqf1olemnanb  10720  seqf1oglem1  10736  expnegzap  10790  nn0ltexp2  10926  hashen  11001  hashunlem  11021  hashprg  11025  leisorel  11054  zfz1isolemiso  11056  seq3coll  11059  swrdccat3b  11267  caucvgrelemrec  11485  resqrexlemex  11531  minmax  11736  xrminmax  11771  fsum2dlemstep  11940  fisumcom2  11944  zproddc  12085  fprod2dlemstep  12128  fprodcom2fi  12132  bezoutlemmain  12514  sqgcd  12545  pcpremul  12811  pceulem  12812  pceu  12813  pczpre  12815  pcdiv  12820  pcqmul  12821  pcqdiv  12825  pcexp  12827  pcdvdsb  12838  pcneg  12843  pcdvdstr  12845  pcgcd1  12846  pc2dvds  12848  pcz  12850  pcaddlem  12857  pcadd  12858  qexpz  12870  expnprm  12871  infpnlem2  12878  f1ocpbllem  13338  f1ovscpbl  13340  sgrppropd  13441  mndpropd  13468  grpsubpropd2  13633  f1ghm0to0  13804  ablnnncan  13855  rngpropd  13913  ringpropd  13996  lmodprop2d  14306  lsspropdg  14389  neiint  14813  restbasg  14836  iscnp4  14886  cnconst2  14901  cnpdis  14910  neitx  14936  upxp  14940  hmeoimaf1o  14982  blssexps  15097  blssex  15098  ssblex  15099  bdmopn  15172  xmettx  15178  metcnp3  15179  tgioo  15222  tgqioo  15223  dvmptfsum  15393  elply2  15403  sin0pilem2  15450  logbgcd1irr  15635  perfect  15669  lgsval  15677  lgsfcl2  15679  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  1dom1el  16312  pwle2  16323