Theorem syl12anc 1271

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  1274  cocan1  5927  fliftfun  5936  isopolem  5962  f1oiso2  5967  caovcld  6175  caovcomd  6178  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  1dom1el  6992  fidceq  7055  findcard2d  7079  diffifi  7082  tridc  7088  en2eqpr  7098  sbthlemi9  7163  supisolem  7206  ordiso2  7233  difinfsnlem  7297  difinfsn  7298  pr2cv1  7399  prarloclemup  7714  prarloc  7722  nqprl  7770  nqpru  7771  ltaddpr  7816  aptiprlemu  7859  archpr  7862  cauappcvgprlem2  7879  caucvgprlem2  7899  caucvgprprlem2  7929  suplocexprlemlub  7943  suplocexpr  7944  recexgt0sr  7992  archsr  8001  axpre-suploclemres  8120  conjmulap  8908  lerec2  9068  ledivp1  9082  cju  9140  nn2ge  9175  gtndiv  9574  supinfneg  9828  infsupneg  9829  z2ge  10060  iccssioo2  10180  fzrev3  10321  elfz1b  10324  zsupcllemstep  10488  zsupssdc  10497  exbtwnzlemstep  10506  exbtwnzlemex  10508  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnre  10515  flqdiv  10582  frec2uzled  10690  seq3caopr  10756  seqcaoprg  10757  iseqf1olemab  10763  iseqf1olemnanb  10764  seqf1oglem1  10780  expnegzap  10834  nn0ltexp2  10970  hashen  11045  hashunlem  11066  hashprg  11071  leisorel  11100  zfz1isolemiso  11102  seq3coll  11105  swrdccat3b  11320  caucvgrelemrec  11539  resqrexlemex  11585  minmax  11790  xrminmax  11825  fsum2dlemstep  11994  fisumcom2  11998  zproddc  12139  fprod2dlemstep  12182  fprodcom2fi  12186  bezoutlemmain  12568  sqgcd  12599  pcpremul  12865  pceulem  12866  pceu  12867  pczpre  12869  pcdiv  12874  pcqmul  12875  pcqdiv  12879  pcexp  12881  pcdvdsb  12892  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pc2dvds  12902  pcz  12904  pcaddlem  12911  pcadd  12912  qexpz  12924  expnprm  12925  infpnlem2  12932  f1ocpbllem  13392  f1ovscpbl  13394  sgrppropd  13495  mndpropd  13522  grpsubpropd2  13687  f1ghm0to0  13858  ablnnncan  13909  rngpropd  13967  ringpropd  14050  lmodprop2d  14361  lsspropdg  14444  neiint  14868  restbasg  14891  iscnp4  14941  cnconst2  14956  cnpdis  14965  neitx  14991  upxp  14995  hmeoimaf1o  15037  blssexps  15152  blssex  15153  ssblex  15154  bdmopn  15227  xmettx  15233  metcnp3  15234  tgioo  15277  tgqioo  15278  dvmptfsum  15448  elply2  15458  sin0pilem2  15505  logbgcd1irr  15690  perfect  15724  lgsval  15732  lgsfcl2  15734  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  clwwlknonex2e  16290  pwle2  16599