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  5917  fliftfun  5926  isopolem  5952  f1oiso2  5957  caovcld  6165  caovcomd  6168  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  fidceq  7039  findcard2d  7061  diffifi  7064  tridc  7070  en2eqpr  7080  sbthlemi9  7143  supisolem  7186  ordiso2  7213  difinfsnlem  7277  difinfsn  7278  pr2cv1  7379  prarloclemup  7693  prarloc  7701  nqprl  7749  nqpru  7750  ltaddpr  7795  aptiprlemu  7838  archpr  7841  cauappcvgprlem2  7858  caucvgprlem2  7878  caucvgprprlem2  7908  suplocexprlemlub  7922  suplocexpr  7923  recexgt0sr  7971  archsr  7980  axpre-suploclemres  8099  conjmulap  8887  lerec2  9047  ledivp1  9061  cju  9119  nn2ge  9154  gtndiv  9553  supinfneg  9802  infsupneg  9803  z2ge  10034  iccssioo2  10154  fzrev3  10295  elfz1b  10298  zsupcllemstep  10461  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnre  10488  flqdiv  10555  frec2uzled  10663  seq3caopr  10729  seqcaoprg  10730  iseqf1olemab  10736  iseqf1olemnanb  10737  seqf1oglem1  10753  expnegzap  10807  nn0ltexp2  10943  hashen  11018  hashunlem  11038  hashprg  11043  leisorel  11072  zfz1isolemiso  11074  seq3coll  11077  swrdccat3b  11287  caucvgrelemrec  11505  resqrexlemex  11551  minmax  11756  xrminmax  11791  fsum2dlemstep  11960  fisumcom2  11964  zproddc  12105  fprod2dlemstep  12148  fprodcom2fi  12152  bezoutlemmain  12534  sqgcd  12565  pcpremul  12831  pceulem  12832  pceu  12833  pczpre  12835  pcdiv  12840  pcqmul  12841  pcqdiv  12845  pcexp  12847  pcdvdsb  12858  pcneg  12863  pcdvdstr  12865  pcgcd1  12866  pc2dvds  12868  pcz  12870  pcaddlem  12877  pcadd  12878  qexpz  12890  expnprm  12891  infpnlem2  12898  f1ocpbllem  13358  f1ovscpbl  13360  sgrppropd  13461  mndpropd  13488  grpsubpropd2  13653  f1ghm0to0  13824  ablnnncan  13875  rngpropd  13933  ringpropd  14016  lmodprop2d  14327  lsspropdg  14410  neiint  14834  restbasg  14857  iscnp4  14907  cnconst2  14922  cnpdis  14931  neitx  14957  upxp  14961  hmeoimaf1o  15003  blssexps  15118  blssex  15119  ssblex  15120  bdmopn  15193  xmettx  15199  metcnp3  15200  tgioo  15243  tgqioo  15244  dvmptfsum  15414  elply2  15424  sin0pilem2  15471  logbgcd1irr  15656  perfect  15690  lgsval  15698  lgsfcl2  15700  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  1dom1el  16409  pwle2  16423