Theorem syl12anc 1247

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  1250  cocan1  5834  fliftfun  5843  isopolem  5869  f1oiso2  5874  caovcld  6077  caovcomd  6080  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  fidceq  6930  findcard2d  6952  diffifi  6955  tridc  6960  en2eqpr  6968  sbthlemi9  7031  supisolem  7074  ordiso2  7101  difinfsnlem  7165  difinfsn  7166  prarloclemup  7562  prarloc  7570  nqprl  7618  nqpru  7619  ltaddpr  7664  aptiprlemu  7707  archpr  7710  cauappcvgprlem2  7727  caucvgprlem2  7747  caucvgprprlem2  7777  suplocexprlemlub  7791  suplocexpr  7792  recexgt0sr  7840  archsr  7849  axpre-suploclemres  7968  conjmulap  8756  lerec2  8916  ledivp1  8930  cju  8988  nn2ge  9023  gtndiv  9421  supinfneg  9669  infsupneg  9670  z2ge  9901  iccssioo2  10021  fzrev3  10162  elfz1b  10165  zsupcllemstep  10319  zsupssdc  10328  exbtwnzlemstep  10337  exbtwnzlemex  10339  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnre  10346  flqdiv  10413  frec2uzled  10521  seq3caopr  10587  seqcaoprg  10588  iseqf1olemab  10594  iseqf1olemnanb  10595  seqf1oglem1  10611  expnegzap  10665  nn0ltexp2  10801  hashen  10876  hashunlem  10896  hashprg  10900  leisorel  10929  zfz1isolemiso  10931  seq3coll  10934  caucvgrelemrec  11144  resqrexlemex  11190  minmax  11395  xrminmax  11430  fsum2dlemstep  11599  fisumcom2  11603  zproddc  11744  fprod2dlemstep  11787  fprodcom2fi  11791  bezoutlemmain  12165  sqgcd  12196  pcpremul  12462  pceulem  12463  pceu  12464  pczpre  12466  pcdiv  12471  pcqmul  12472  pcqdiv  12476  pcexp  12478  pcdvdsb  12489  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  pcz  12501  pcaddlem  12508  pcadd  12509  qexpz  12521  expnprm  12522  infpnlem2  12529  f1ocpbllem  12953  f1ovscpbl  12955  sgrppropd  13056  mndpropd  13081  grpsubpropd2  13237  f1ghm0to0  13402  ablnnncan  13453  rngpropd  13511  ringpropd  13594  lmodprop2d  13904  lsspropdg  13987  neiint  14381  restbasg  14404  iscnp4  14454  cnconst2  14469  cnpdis  14478  neitx  14504  upxp  14508  hmeoimaf1o  14550  blssexps  14665  blssex  14666  ssblex  14667  bdmopn  14740  xmettx  14746  metcnp3  14747  tgioo  14790  tgqioo  14791  dvmptfsum  14961  elply2  14971  sin0pilem2  15018  logbgcd1irr  15203  perfect  15237  lgsval  15245  lgsfcl2  15247  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  1dom1el  15637  pwle2  15643