Theorem syl12anc 1197

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 306	. 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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  syl22anc  1200  cocan1  5642  fliftfun  5651  isopolem  5677  f1oiso2  5682  caovcld  5878  caovcomd  5881  tfrlemisucaccv  6176  tfr1onlemsucaccv  6192  tfr1onlembxssdm  6194  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  fidceq  6716  findcard2d  6738  diffifi  6741  tridc  6746  en2eqpr  6754  sbthlemi9  6805  supisolem  6847  ordiso2  6872  difinfsnlem  6936  difinfsn  6937  prarloclemup  7251  prarloc  7259  nqprl  7307  nqpru  7308  ltaddpr  7353  aptiprlemu  7396  archpr  7399  cauappcvgprlem2  7416  caucvgprlem2  7436  caucvgprprlem2  7466  recexgt0sr  7516  archsr  7524  conjmulap  8402  lerec2  8557  ledivp1  8571  cju  8629  nn2ge  8663  gtndiv  9050  supinfneg  9292  infsupneg  9293  z2ge  9502  iccssioo2  9622  fzrev3  9760  elfz1b  9763  exbtwnzlemstep  9918  exbtwnzlemex  9920  rebtwn2zlemstep  9923  rebtwn2z  9925  qbtwnre  9927  flqdiv  9987  frec2uzled  10095  seq3caopr  10149  iseqf1olemab  10155  iseqf1olemnanb  10156  expnegzap  10220  hashen  10423  hashunlem  10443  hashprg  10447  leisorel  10473  zfz1isolemiso  10475  seq3coll  10478  caucvgrelemrec  10643  resqrexlemex  10689  minmax  10893  xrminmax  10926  fsum2dlemstep  11095  fisumcom2  11099  zsupcllemstep  11486  bezoutlemmain  11532  sqgcd  11563  neiint  12157  restbasg  12180  iscnp4  12229  cnconst2  12244  cnpdis  12253  neitx  12279  upxp  12283  blssexps  12418  blssex  12419  ssblex  12420  bdmopn  12493  xmettx  12499  metcnp3  12500  tgioo  12532  tgqioo  12533  pwle2  12885