Theorem syl12anc 1231

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 308	. 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 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  syl22anc  1234  cocan1  5766  fliftfun  5775  isopolem  5801  f1oiso2  5806  caovcld  6006  caovcomd  6009  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  fidceq  6847  findcard2d  6869  diffifi  6872  tridc  6877  en2eqpr  6885  sbthlemi9  6942  supisolem  6985  ordiso2  7012  difinfsnlem  7076  difinfsn  7077  prarloclemup  7457  prarloc  7465  nqprl  7513  nqpru  7514  ltaddpr  7559  aptiprlemu  7602  archpr  7605  cauappcvgprlem2  7622  caucvgprlem2  7642  caucvgprprlem2  7672  suplocexprlemlub  7686  suplocexpr  7687  recexgt0sr  7735  archsr  7744  axpre-suploclemres  7863  conjmulap  8646  lerec2  8805  ledivp1  8819  cju  8877  nn2ge  8911  gtndiv  9307  supinfneg  9554  infsupneg  9555  z2ge  9783  iccssioo2  9903  fzrev3  10043  elfz1b  10046  exbtwnzlemstep  10204  exbtwnzlemex  10206  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnre  10213  flqdiv  10277  frec2uzled  10385  seq3caopr  10439  iseqf1olemab  10445  iseqf1olemnanb  10446  expnegzap  10510  nn0ltexp2  10644  hashen  10718  hashunlem  10739  hashprg  10743  leisorel  10772  zfz1isolemiso  10774  seq3coll  10777  caucvgrelemrec  10943  resqrexlemex  10989  minmax  11193  xrminmax  11228  fsum2dlemstep  11397  fisumcom2  11401  zproddc  11542  fprod2dlemstep  11585  fprodcom2fi  11589  zsupcllemstep  11900  zsupssdc  11909  bezoutlemmain  11953  sqgcd  11984  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pcdiv  12256  pcqmul  12257  pcqdiv  12261  pcexp  12263  pcdvdsb  12273  pcneg  12278  pcdvdstr  12280  pcgcd1  12281  pc2dvds  12283  pcz  12285  pcaddlem  12292  pcadd  12293  qexpz  12304  expnprm  12305  infpnlem2  12312  mndpropd  12676  neiint  12939  restbasg  12962  iscnp4  13012  cnconst2  13027  cnpdis  13036  neitx  13062  upxp  13066  hmeoimaf1o  13108  blssexps  13223  blssex  13224  ssblex  13225  bdmopn  13298  xmettx  13304  metcnp3  13305  tgioo  13340  tgqioo  13341  sin0pilem2  13497  logbgcd1irr  13679  lgsval  13699  lgsfcl2  13701  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  pwle2  14031