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  5830  fliftfun  5839  isopolem  5865  f1oiso2  5870  caovcld  6072  caovcomd  6075  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  fidceq  6925  findcard2d  6947  diffifi  6950  tridc  6955  en2eqpr  6963  sbthlemi9  7024  supisolem  7067  ordiso2  7094  difinfsnlem  7158  difinfsn  7159  prarloclemup  7555  prarloc  7563  nqprl  7611  nqpru  7612  ltaddpr  7657  aptiprlemu  7700  archpr  7703  cauappcvgprlem2  7720  caucvgprlem2  7740  caucvgprprlem2  7770  suplocexprlemlub  7784  suplocexpr  7785  recexgt0sr  7833  archsr  7842  axpre-suploclemres  7961  conjmulap  8748  lerec2  8908  ledivp1  8922  cju  8980  nn2ge  9015  gtndiv  9412  supinfneg  9660  infsupneg  9661  z2ge  9892  iccssioo2  10012  fzrev3  10153  elfz1b  10156  exbtwnzlemstep  10316  exbtwnzlemex  10318  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnre  10325  flqdiv  10392  frec2uzled  10500  seq3caopr  10566  seqcaoprg  10567  iseqf1olemab  10573  iseqf1olemnanb  10574  seqf1oglem1  10590  expnegzap  10644  nn0ltexp2  10780  hashen  10855  hashunlem  10875  hashprg  10879  leisorel  10908  zfz1isolemiso  10910  seq3coll  10913  caucvgrelemrec  11123  resqrexlemex  11169  minmax  11373  xrminmax  11408  fsum2dlemstep  11577  fisumcom2  11581  zproddc  11722  fprod2dlemstep  11765  fprodcom2fi  11769  zsupcllemstep  12082  zsupssdc  12091  bezoutlemmain  12135  sqgcd  12166  pcpremul  12431  pceulem  12432  pceu  12433  pczpre  12435  pcdiv  12440  pcqmul  12441  pcqdiv  12445  pcexp  12447  pcdvdsb  12458  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pc2dvds  12468  pcz  12470  pcaddlem  12477  pcadd  12478  qexpz  12490  expnprm  12491  infpnlem2  12498  f1ocpbllem  12893  f1ovscpbl  12895  sgrppropd  12996  mndpropd  13021  grpsubpropd2  13177  f1ghm0to0  13342  ablnnncan  13393  rngpropd  13451  ringpropd  13534  lmodprop2d  13844  lsspropdg  13927  neiint  14313  restbasg  14336  iscnp4  14386  cnconst2  14401  cnpdis  14410  neitx  14436  upxp  14440  hmeoimaf1o  14482  blssexps  14597  blssex  14598  ssblex  14599  bdmopn  14672  xmettx  14678  metcnp3  14679  tgioo  14714  tgqioo  14715  elply2  14881  sin0pilem2  14917  logbgcd1irr  15099  lgsval  15120  lgsfcl2  15122  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  1dom1el  15483  pwle2  15489