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  5960  fliftfun  5969  isopolem  5995  f1oiso2  6000  caovcld  6208  caovcomd  6211  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  1dom1el  7060  fidceq  7124  findcard2d  7148  diffifi  7151  tridc  7157  en2eqpr  7167  sbthlemi9  7235  supisolem  7299  ordiso2  7326  difinfsnlem  7390  difinfsn  7391  pr2cv1  7492  prarloclemup  7810  prarloc  7818  nqprl  7866  nqpru  7867  ltaddpr  7912  aptiprlemu  7955  archpr  7958  cauappcvgprlem2  7975  caucvgprlem2  7995  caucvgprprlem2  8025  suplocexprlemlub  8039  suplocexpr  8040  recexgt0sr  8088  archsr  8097  axpre-suploclemres  8216  conjmulap  9003  lerec2  9163  ledivp1  9177  cju  9235  nn2ge  9270  gtndiv  9673  supinfneg  9927  infsupneg  9928  z2ge  10159  iccssioo2  10279  fzrev3  10421  elfz1b  10424  zsupcllemstep  10589  zsupssdc  10598  exbtwnzlemstep  10607  exbtwnzlemex  10609  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnre  10616  flqdiv  10683  frec2uzled  10791  seq3caopr  10857  seqcaoprg  10858  iseqf1olemab  10864  iseqf1olemnanb  10865  seqf1oglem1  10881  expnegzap  10935  nn0ltexp2  11071  hashen  11147  hashunlem  11168  hashprg  11173  hashfibclem  11206  leisorel  11209  zfz1isolemiso  11211  seq3coll  11214  swrdccat3b  11432  caucvgrelemrec  11664  resqrexlemex  11710  minmax  11915  xrminmax  11950  fsum2dlemstep  12120  fisumcom2  12124  zproddc  12265  fprod2dlemstep  12308  fprodcom2fi  12312  bezoutlemmain  12694  sqgcd  12725  pcpremul  12991  pceulem  12992  pceu  12993  pczpre  12995  pcdiv  13000  pcqmul  13001  pcqdiv  13005  pcexp  13007  pcdvdsb  13018  pcneg  13023  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcz  13030  pcaddlem  13037  pcadd  13038  qexpz  13050  expnprm  13051  infpnlem2  13058  f1ocpbllem  13523  f1ovscpbl  13525  sgrppropd  13626  mndpropd  13653  grpsubpropd2  13818  f1ghm0to0  13989  ablnnncan  14040  rngpropd  14099  ringpropd  14182  lmodprop2d  14496  lsspropdg  14579  neiint  15010  restbasg  15033  iscnp4  15083  cnconst2  15098  cnpdis  15107  neitx  15133  upxp  15137  hmeoimaf1o  15179  blssexps  15294  blssex  15295  ssblex  15296  bdmopn  15369  xmettx  15375  metcnp3  15376  tgioo  15419  tgqioo  15420  dvmptfsum  15590  elply2  15600  sin0pilem2  15647  logbgcd1irr  15832  perfect  15869  lgsval  15877  lgsfcl2  15879  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  clwwlknonex2e  16435  pwle2  16772  qdiff  16833