Theorem syl12anc 1167

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 303	. 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 102

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

This theorem is referenced by:  syl22anc  1170  cocan1  5447  fliftfun  5456  isopolem  5481  f1oiso2  5486  caovcld  5674  caovcomd  5677  tfrlemisucaccv  5962  fidceq  6354  findcard2d  6375  diffifi  6378  en2eqpr  6380  supisolem  6421  ordiso2  6446  prarloclemup  6685  prarloc  6693  nqprl  6741  nqpru  6742  ltaddpr  6787  aptiprlemu  6830  archpr  6833  cauappcvgprlem2  6850  caucvgprlem2  6870  caucvgprprlem2  6900  recexgt0sr  6950  archsr  6958  conjmulap  7817  lerec2  7967  ledivp1  7981  cju  8038  nn2ge  8071  gtndiv  8442  supinfneg  8683  infsupneg  8684  z2ge  8893  iccssioo2  8969  fzrev3  9104  elfz1b  9107  qbtwnzlemstep  9257  qbtwnzlemex  9259  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnre  9265  flqdiv  9323  iseqcaopr  9462  expnegzap  9510  caucvgrelemrec  9865  resqrexlemex  9911  minmax  10112  zsupcllemstep  10341  bezoutlemmain  10387  sqgcd  10418