Theorem syl12anc 1272

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  1275  cocan1  5938  fliftfun  5947  isopolem  5973  f1oiso2  5978  caovcld  6186  caovcomd  6189  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  1dom1el  7036  fidceq  7099  findcard2d  7123  diffifi  7126  tridc  7132  en2eqpr  7142  sbthlemi9  7207  supisolem  7250  ordiso2  7277  difinfsnlem  7341  difinfsn  7342  pr2cv1  7443  prarloclemup  7758  prarloc  7766  nqprl  7814  nqpru  7815  ltaddpr  7860  aptiprlemu  7903  archpr  7906  cauappcvgprlem2  7923  caucvgprlem2  7943  caucvgprprlem2  7973  suplocexprlemlub  7987  suplocexpr  7988  recexgt0sr  8036  archsr  8045  axpre-suploclemres  8164  conjmulap  8951  lerec2  9111  ledivp1  9125  cju  9183  nn2ge  9218  gtndiv  9619  supinfneg  9873  infsupneg  9874  z2ge  10105  iccssioo2  10225  fzrev3  10367  elfz1b  10370  zsupcllemstep  10535  zsupssdc  10544  exbtwnzlemstep  10553  exbtwnzlemex  10555  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnre  10562  flqdiv  10629  frec2uzled  10737  seq3caopr  10803  seqcaoprg  10804  iseqf1olemab  10810  iseqf1olemnanb  10811  seqf1oglem1  10827  expnegzap  10881  nn0ltexp2  11017  hashen  11092  hashunlem  11113  hashprg  11118  leisorel  11147  zfz1isolemiso  11149  seq3coll  11152  swrdccat3b  11370  caucvgrelemrec  11602  resqrexlemex  11648  minmax  11853  xrminmax  11888  fsum2dlemstep  12058  fisumcom2  12062  zproddc  12203  fprod2dlemstep  12246  fprodcom2fi  12250  bezoutlemmain  12632  sqgcd  12663  pcpremul  12929  pceulem  12930  pceu  12931  pczpre  12933  pcdiv  12938  pcqmul  12939  pcqdiv  12943  pcexp  12945  pcdvdsb  12956  pcneg  12961  pcdvdstr  12963  pcgcd1  12964  pc2dvds  12966  pcz  12968  pcaddlem  12975  pcadd  12976  qexpz  12988  expnprm  12989  infpnlem2  12996  f1ocpbllem  13456  f1ovscpbl  13458  sgrppropd  13559  mndpropd  13586  grpsubpropd2  13751  f1ghm0to0  13922  ablnnncan  13973  rngpropd  14032  ringpropd  14115  lmodprop2d  14427  lsspropdg  14510  neiint  14939  restbasg  14962  iscnp4  15012  cnconst2  15027  cnpdis  15036  neitx  15062  upxp  15066  hmeoimaf1o  15108  blssexps  15223  blssex  15224  ssblex  15225  bdmopn  15298  xmettx  15304  metcnp3  15305  tgioo  15348  tgqioo  15349  dvmptfsum  15519  elply2  15529  sin0pilem2  15576  logbgcd1irr  15761  perfect  15798  lgsval  15806  lgsfcl2  15808  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  clwwlknonex2e  16364  pwle2  16703  qdiff  16764