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  5855  fliftfun  5864  isopolem  5890  f1oiso2  5895  caovcld  6099  caovcomd  6102  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfr1onlembxssdm  6428  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  fidceq  6965  findcard2d  6987  diffifi  6990  tridc  6995  en2eqpr  7003  sbthlemi9  7066  supisolem  7109  ordiso2  7136  difinfsnlem  7200  difinfsn  7201  prarloclemup  7607  prarloc  7615  nqprl  7663  nqpru  7664  ltaddpr  7709  aptiprlemu  7752  archpr  7755  cauappcvgprlem2  7772  caucvgprlem2  7792  caucvgprprlem2  7822  suplocexprlemlub  7836  suplocexpr  7837  recexgt0sr  7885  archsr  7894  axpre-suploclemres  8013  conjmulap  8801  lerec2  8961  ledivp1  8975  cju  9033  nn2ge  9068  gtndiv  9467  supinfneg  9715  infsupneg  9716  z2ge  9947  iccssioo2  10067  fzrev3  10208  elfz1b  10211  zsupcllemstep  10370  zsupssdc  10379  exbtwnzlemstep  10388  exbtwnzlemex  10390  rebtwn2zlemstep  10393  rebtwn2z  10395  qbtwnre  10397  flqdiv  10464  frec2uzled  10572  seq3caopr  10638  seqcaoprg  10639  iseqf1olemab  10645  iseqf1olemnanb  10646  seqf1oglem1  10662  expnegzap  10716  nn0ltexp2  10852  hashen  10927  hashunlem  10947  hashprg  10951  leisorel  10980  zfz1isolemiso  10982  seq3coll  10985  caucvgrelemrec  11261  resqrexlemex  11307  minmax  11512  xrminmax  11547  fsum2dlemstep  11716  fisumcom2  11720  zproddc  11861  fprod2dlemstep  11904  fprodcom2fi  11908  bezoutlemmain  12290  sqgcd  12321  pcpremul  12587  pceulem  12588  pceu  12589  pczpre  12591  pcdiv  12596  pcqmul  12597  pcqdiv  12601  pcexp  12603  pcdvdsb  12614  pcneg  12619  pcdvdstr  12621  pcgcd1  12622  pc2dvds  12624  pcz  12626  pcaddlem  12633  pcadd  12634  qexpz  12646  expnprm  12647  infpnlem2  12654  f1ocpbllem  13113  f1ovscpbl  13115  sgrppropd  13216  mndpropd  13243  grpsubpropd2  13408  f1ghm0to0  13579  ablnnncan  13630  rngpropd  13688  ringpropd  13771  lmodprop2d  14081  lsspropdg  14164  neiint  14588  restbasg  14611  iscnp4  14661  cnconst2  14676  cnpdis  14685  neitx  14711  upxp  14715  hmeoimaf1o  14757  blssexps  14872  blssex  14873  ssblex  14874  bdmopn  14947  xmettx  14953  metcnp3  14954  tgioo  14997  tgqioo  14998  dvmptfsum  15168  elply2  15178  sin0pilem2  15225  logbgcd1irr  15410  perfect  15444  lgsval  15452  lgsfcl2  15454  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  1dom1el  15889  pwle2  15897