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  5879  fliftfun  5888  isopolem  5914  f1oiso2  5919  caovcld  6123  caovcomd  6126  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  fidceq  6992  findcard2d  7014  diffifi  7017  tridc  7022  en2eqpr  7030  sbthlemi9  7093  supisolem  7136  ordiso2  7163  difinfsnlem  7227  difinfsn  7228  pr2cv1  7329  prarloclemup  7643  prarloc  7651  nqprl  7699  nqpru  7700  ltaddpr  7745  aptiprlemu  7788  archpr  7791  cauappcvgprlem2  7808  caucvgprlem2  7828  caucvgprprlem2  7858  suplocexprlemlub  7872  suplocexpr  7873  recexgt0sr  7921  archsr  7930  axpre-suploclemres  8049  conjmulap  8837  lerec2  8997  ledivp1  9011  cju  9069  nn2ge  9104  gtndiv  9503  supinfneg  9751  infsupneg  9752  z2ge  9983  iccssioo2  10103  fzrev3  10244  elfz1b  10247  zsupcllemstep  10409  zsupssdc  10418  exbtwnzlemstep  10427  exbtwnzlemex  10429  rebtwn2zlemstep  10432  rebtwn2z  10434  qbtwnre  10436  flqdiv  10503  frec2uzled  10611  seq3caopr  10677  seqcaoprg  10678  iseqf1olemab  10684  iseqf1olemnanb  10685  seqf1oglem1  10701  expnegzap  10755  nn0ltexp2  10891  hashen  10966  hashunlem  10986  hashprg  10990  leisorel  11019  zfz1isolemiso  11021  seq3coll  11024  swrdccat3b  11231  caucvgrelemrec  11405  resqrexlemex  11451  minmax  11656  xrminmax  11691  fsum2dlemstep  11860  fisumcom2  11864  zproddc  12005  fprod2dlemstep  12048  fprodcom2fi  12052  bezoutlemmain  12434  sqgcd  12465  pcpremul  12731  pceulem  12732  pceu  12733  pczpre  12735  pcdiv  12740  pcqmul  12741  pcqdiv  12745  pcexp  12747  pcdvdsb  12758  pcneg  12763  pcdvdstr  12765  pcgcd1  12766  pc2dvds  12768  pcz  12770  pcaddlem  12777  pcadd  12778  qexpz  12790  expnprm  12791  infpnlem2  12798  f1ocpbllem  13257  f1ovscpbl  13259  sgrppropd  13360  mndpropd  13387  grpsubpropd2  13552  f1ghm0to0  13723  ablnnncan  13774  rngpropd  13832  ringpropd  13915  lmodprop2d  14225  lsspropdg  14308  neiint  14732  restbasg  14755  iscnp4  14805  cnconst2  14820  cnpdis  14829  neitx  14855  upxp  14859  hmeoimaf1o  14901  blssexps  15016  blssex  15017  ssblex  15018  bdmopn  15091  xmettx  15097  metcnp3  15098  tgioo  15141  tgqioo  15142  dvmptfsum  15312  elply2  15322  sin0pilem2  15369  logbgcd1irr  15554  perfect  15588  lgsval  15596  lgsfcl2  15598  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  1dom1el  16126  pwle2  16137