Theorem syl12anc 1276

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  syl22anc  1279  cocan1  5993  fliftfun  6002  isopolem  6028  f1oiso2  6033  caovcld  6243  caovcomd  6246  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  1dom1el  7107  fidceq  7171  findcard2d  7195  diffifi  7198  tridc  7204  en2eqpr  7214  sbthlemi9  7282  supisolem  7348  ordiso2  7375  difinfsnlem  7439  difinfsn  7440  pr2cv1  7541  prarloclemup  7862  prarloc  7870  nqprl  7918  nqpru  7919  ltaddpr  7964  aptiprlemu  8007  archpr  8010  cauappcvgprlem2  8027  caucvgprlem2  8047  caucvgprprlem2  8077  suplocexprlemlub  8091  suplocexpr  8092  recexgt0sr  8140  archsr  8149  axpre-suploclemres  8268  conjmulap  9059  lerec2  9219  ledivp1  9233  cju  9291  nn2ge  9337  gtndiv  9741  supinfneg  9995  infsupneg  9996  z2ge  10228  iccssioo2  10348  fzrev3  10494  elfz1b  10497  zsupcllemstep  10662  zsupssdc  10673  exbtwnzlemstep  10682  exbtwnzlemex  10684  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnre  10691  flqdiv  10758  frec2uzled  10866  seq3caopr  10932  seqcaoprg  10933  iseqf1olemab  10939  iseqf1olemnanb  10940  seqf1oglem1  10956  expnegzap  11010  nn0ltexp2  11147  hashen  11223  hashunlem  11244  hashprg  11249  hashfibclem  11282  hashf1lem2  11286  leisorel  11289  zfz1isolemiso  11291  seq3coll  11294  swrdccat3b  11512  caucvgrelemrec  11745  resqrexlemex  11791  minmax  11996  xrminmax  12031  fsum2dlemstep  12201  fisumcom2  12205  zproddc  12346  fprod2dlemstep  12389  fprodcom2fi  12393  bezoutlemmain  12775  sqgcd  12806  pcpremul  13072  pceulem  13073  pceu  13074  pczpre  13076  pcdiv  13081  pcqmul  13082  pcqdiv  13086  pcexp  13088  pcdvdsb  13099  pcneg  13104  pcdvdstr  13106  pcgcd1  13107  pc2dvds  13109  pcz  13111  pcaddlem  13118  pcadd  13119  qexpz  13131  expnprm  13132  infpnlem2  13139  ballotfilemfc0  13232  ballotfilemfcc  13233  f1ocpbllem  13631  f1ovscpbl  13633  sgrppropd  13728  mndpropd  13753  grpsubpropd2  13910  f1ghm0to0  14075  ablnnncan  14127  rngpropd  14254  ringpropd  14343  lmodprop2d  14685  lsspropdg  14768  assapropd  15014  neiint  15246  restbasg  15269  iscnp4  15319  cnconst2  15334  cnpdis  15343  neitx  15369  upxp  15373  hmeoimaf1o  15415  blssexps  15530  blssex  15531  ssblex  15532  bdmopn  15605  xmettx  15611  metcnp3  15612  tgioo  15655  tgqioo  15656  dvmptfsum  15826  elply2  15836  sin0pilem2  15883  logbgcd1irr  16069  perfect  16115  lgsval  16123  lgsfcl2  16125  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  clwwlknonex2e  16681  pwle2  17028  qdiff  17098