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  5923  fliftfun  5932  isopolem  5958  f1oiso2  5963  caovcld  6171  caovcomd  6174  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  1dom1el  6988  fidceq  7051  findcard2d  7073  diffifi  7076  tridc  7082  en2eqpr  7092  sbthlemi9  7155  supisolem  7198  ordiso2  7225  difinfsnlem  7289  difinfsn  7290  pr2cv1  7391  prarloclemup  7705  prarloc  7713  nqprl  7761  nqpru  7762  ltaddpr  7807  aptiprlemu  7850  archpr  7853  cauappcvgprlem2  7870  caucvgprlem2  7890  caucvgprprlem2  7920  suplocexprlemlub  7934  suplocexpr  7935  recexgt0sr  7983  archsr  7992  axpre-suploclemres  8111  conjmulap  8899  lerec2  9059  ledivp1  9073  cju  9131  nn2ge  9166  gtndiv  9565  supinfneg  9819  infsupneg  9820  z2ge  10051  iccssioo2  10171  fzrev3  10312  elfz1b  10315  zsupcllemstep  10479  zsupssdc  10488  exbtwnzlemstep  10497  exbtwnzlemex  10499  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnre  10506  flqdiv  10573  frec2uzled  10681  seq3caopr  10747  seqcaoprg  10748  iseqf1olemab  10754  iseqf1olemnanb  10755  seqf1oglem1  10771  expnegzap  10825  nn0ltexp2  10961  hashen  11036  hashunlem  11057  hashprg  11062  leisorel  11091  zfz1isolemiso  11093  seq3coll  11096  swrdccat3b  11311  caucvgrelemrec  11530  resqrexlemex  11576  minmax  11781  xrminmax  11816  fsum2dlemstep  11985  fisumcom2  11989  zproddc  12130  fprod2dlemstep  12173  fprodcom2fi  12177  bezoutlemmain  12559  sqgcd  12590  pcpremul  12856  pceulem  12857  pceu  12858  pczpre  12860  pcdiv  12865  pcqmul  12866  pcqdiv  12870  pcexp  12872  pcdvdsb  12883  pcneg  12888  pcdvdstr  12890  pcgcd1  12891  pc2dvds  12893  pcz  12895  pcaddlem  12902  pcadd  12903  qexpz  12915  expnprm  12916  infpnlem2  12923  f1ocpbllem  13383  f1ovscpbl  13385  sgrppropd  13486  mndpropd  13513  grpsubpropd2  13678  f1ghm0to0  13849  ablnnncan  13900  rngpropd  13958  ringpropd  14041  lmodprop2d  14352  lsspropdg  14435  neiint  14859  restbasg  14882  iscnp4  14932  cnconst2  14947  cnpdis  14956  neitx  14982  upxp  14986  hmeoimaf1o  15028  blssexps  15143  blssex  15144  ssblex  15145  bdmopn  15218  xmettx  15224  metcnp3  15225  tgioo  15268  tgqioo  15269  dvmptfsum  15439  elply2  15449  sin0pilem2  15496  logbgcd1irr  15681  perfect  15715  lgsval  15723  lgsfcl2  15725  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  clwwlknonex2e  16235  pwle2  16535