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  5928  fliftfun  5937  isopolem  5963  f1oiso2  5968  caovcld  6176  caovcomd  6179  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  1dom1el  6993  fidceq  7056  findcard2d  7080  diffifi  7083  tridc  7089  en2eqpr  7099  sbthlemi9  7164  supisolem  7207  ordiso2  7234  difinfsnlem  7298  difinfsn  7299  pr2cv1  7400  prarloclemup  7715  prarloc  7723  nqprl  7771  nqpru  7772  ltaddpr  7817  aptiprlemu  7860  archpr  7863  cauappcvgprlem2  7880  caucvgprlem2  7900  caucvgprprlem2  7930  suplocexprlemlub  7944  suplocexpr  7945  recexgt0sr  7993  archsr  8002  axpre-suploclemres  8121  conjmulap  8909  lerec2  9069  ledivp1  9083  cju  9141  nn2ge  9176  gtndiv  9575  supinfneg  9829  infsupneg  9830  z2ge  10061  iccssioo2  10181  fzrev3  10322  elfz1b  10325  zsupcllemstep  10490  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnre  10517  flqdiv  10584  frec2uzled  10692  seq3caopr  10758  seqcaoprg  10759  iseqf1olemab  10765  iseqf1olemnanb  10766  seqf1oglem1  10782  expnegzap  10836  nn0ltexp2  10972  hashen  11047  hashunlem  11068  hashprg  11073  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  swrdccat3b  11325  caucvgrelemrec  11544  resqrexlemex  11590  minmax  11795  xrminmax  11830  fsum2dlemstep  12000  fisumcom2  12004  zproddc  12145  fprod2dlemstep  12188  fprodcom2fi  12192  bezoutlemmain  12574  sqgcd  12605  pcpremul  12871  pceulem  12872  pceu  12873  pczpre  12875  pcdiv  12880  pcqmul  12881  pcqdiv  12885  pcexp  12887  pcdvdsb  12898  pcneg  12903  pcdvdstr  12905  pcgcd1  12906  pc2dvds  12908  pcz  12910  pcaddlem  12917  pcadd  12918  qexpz  12930  expnprm  12931  infpnlem2  12938  f1ocpbllem  13398  f1ovscpbl  13400  sgrppropd  13501  mndpropd  13528  grpsubpropd2  13693  f1ghm0to0  13864  ablnnncan  13915  rngpropd  13974  ringpropd  14057  lmodprop2d  14368  lsspropdg  14451  neiint  14875  restbasg  14898  iscnp4  14948  cnconst2  14963  cnpdis  14972  neitx  14998  upxp  15002  hmeoimaf1o  15044  blssexps  15159  blssex  15160  ssblex  15161  bdmopn  15234  xmettx  15240  metcnp3  15241  tgioo  15284  tgqioo  15285  dvmptfsum  15455  elply2  15465  sin0pilem2  15512  logbgcd1irr  15697  perfect  15731  lgsval  15739  lgsfcl2  15741  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  clwwlknonex2e  16297  pwle2  16625  qdiff  16679