Theorem syl12anc 1247

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  1250  cocan1  5831  fliftfun  5840  isopolem  5866  f1oiso2  5871  caovcld  6074  caovcomd  6077  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  fidceq  6927  findcard2d  6949  diffifi  6952  tridc  6957  en2eqpr  6965  sbthlemi9  7026  supisolem  7069  ordiso2  7096  difinfsnlem  7160  difinfsn  7161  prarloclemup  7557  prarloc  7565  nqprl  7613  nqpru  7614  ltaddpr  7659  aptiprlemu  7702  archpr  7705  cauappcvgprlem2  7722  caucvgprlem2  7742  caucvgprprlem2  7772  suplocexprlemlub  7786  suplocexpr  7787  recexgt0sr  7835  archsr  7844  axpre-suploclemres  7963  conjmulap  8750  lerec2  8910  ledivp1  8924  cju  8982  nn2ge  9017  gtndiv  9415  supinfneg  9663  infsupneg  9664  z2ge  9895  iccssioo2  10015  fzrev3  10156  elfz1b  10159  exbtwnzlemstep  10319  exbtwnzlemex  10321  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnre  10328  flqdiv  10395  frec2uzled  10503  seq3caopr  10569  seqcaoprg  10570  iseqf1olemab  10576  iseqf1olemnanb  10577  seqf1oglem1  10593  expnegzap  10647  nn0ltexp2  10783  hashen  10858  hashunlem  10878  hashprg  10882  leisorel  10911  zfz1isolemiso  10913  seq3coll  10916  caucvgrelemrec  11126  resqrexlemex  11172  minmax  11376  xrminmax  11411  fsum2dlemstep  11580  fisumcom2  11584  zproddc  11725  fprod2dlemstep  11768  fprodcom2fi  11772  zsupcllemstep  12085  zsupssdc  12094  bezoutlemmain  12138  sqgcd  12169  pcpremul  12434  pceulem  12435  pceu  12436  pczpre  12438  pcdiv  12443  pcqmul  12444  pcqdiv  12448  pcexp  12450  pcdvdsb  12461  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcz  12473  pcaddlem  12480  pcadd  12481  qexpz  12493  expnprm  12494  infpnlem2  12501  f1ocpbllem  12896  f1ovscpbl  12898  sgrppropd  12999  mndpropd  13024  grpsubpropd2  13180  f1ghm0to0  13345  ablnnncan  13396  rngpropd  13454  ringpropd  13537  lmodprop2d  13847  lsspropdg  13930  neiint  14324  restbasg  14347  iscnp4  14397  cnconst2  14412  cnpdis  14421  neitx  14447  upxp  14451  hmeoimaf1o  14493  blssexps  14608  blssex  14609  ssblex  14610  bdmopn  14683  xmettx  14689  metcnp3  14690  tgioo  14733  tgqioo  14734  dvmptfsum  14904  elply2  14914  sin0pilem2  14958  logbgcd1irr  15140  lgsval  15161  lgsfcl2  15163  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  1dom1el  15553  pwle2  15559