Theorem syl12anc 1248

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  1251  cocan1  5856  fliftfun  5865  isopolem  5891  f1oiso2  5896  caovcld  6100  caovcomd  6103  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  fidceq  6966  findcard2d  6988  diffifi  6991  tridc  6996  en2eqpr  7004  sbthlemi9  7067  supisolem  7110  ordiso2  7137  difinfsnlem  7201  difinfsn  7202  prarloclemup  7608  prarloc  7616  nqprl  7664  nqpru  7665  ltaddpr  7710  aptiprlemu  7753  archpr  7756  cauappcvgprlem2  7773  caucvgprlem2  7793  caucvgprprlem2  7823  suplocexprlemlub  7837  suplocexpr  7838  recexgt0sr  7886  archsr  7895  axpre-suploclemres  8014  conjmulap  8802  lerec2  8962  ledivp1  8976  cju  9034  nn2ge  9069  gtndiv  9468  supinfneg  9716  infsupneg  9717  z2ge  9948  iccssioo2  10068  fzrev3  10209  elfz1b  10212  zsupcllemstep  10372  zsupssdc  10381  exbtwnzlemstep  10390  exbtwnzlemex  10392  rebtwn2zlemstep  10395  rebtwn2z  10397  qbtwnre  10399  flqdiv  10466  frec2uzled  10574  seq3caopr  10640  seqcaoprg  10641  iseqf1olemab  10647  iseqf1olemnanb  10648  seqf1oglem1  10664  expnegzap  10718  nn0ltexp2  10854  hashen  10929  hashunlem  10949  hashprg  10953  leisorel  10982  zfz1isolemiso  10984  seq3coll  10987  caucvgrelemrec  11290  resqrexlemex  11336  minmax  11541  xrminmax  11576  fsum2dlemstep  11745  fisumcom2  11749  zproddc  11890  fprod2dlemstep  11933  fprodcom2fi  11937  bezoutlemmain  12319  sqgcd  12350  pcpremul  12616  pceulem  12617  pceu  12618  pczpre  12620  pcdiv  12625  pcqmul  12626  pcqdiv  12630  pcexp  12632  pcdvdsb  12643  pcneg  12648  pcdvdstr  12650  pcgcd1  12651  pc2dvds  12653  pcz  12655  pcaddlem  12662  pcadd  12663  qexpz  12675  expnprm  12676  infpnlem2  12683  f1ocpbllem  13142  f1ovscpbl  13144  sgrppropd  13245  mndpropd  13272  grpsubpropd2  13437  f1ghm0to0  13608  ablnnncan  13659  rngpropd  13717  ringpropd  13800  lmodprop2d  14110  lsspropdg  14193  neiint  14617  restbasg  14640  iscnp4  14690  cnconst2  14705  cnpdis  14714  neitx  14740  upxp  14744  hmeoimaf1o  14786  blssexps  14901  blssex  14902  ssblex  14903  bdmopn  14976  xmettx  14982  metcnp3  14983  tgioo  15026  tgqioo  15027  dvmptfsum  15197  elply2  15207  sin0pilem2  15254  logbgcd1irr  15439  perfect  15473  lgsval  15481  lgsfcl2  15483  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  1dom1el  15927  pwle2  15935