Theorem syl12anc 1226

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 308	. 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 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  syl22anc  1229  cocan1  5755  fliftfun  5764  isopolem  5790  f1oiso2  5795  caovcld  5995  caovcomd  5998  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  fidceq  6835  findcard2d  6857  diffifi  6860  tridc  6865  en2eqpr  6873  sbthlemi9  6930  supisolem  6973  ordiso2  7000  difinfsnlem  7064  difinfsn  7065  prarloclemup  7436  prarloc  7444  nqprl  7492  nqpru  7493  ltaddpr  7538  aptiprlemu  7581  archpr  7584  cauappcvgprlem2  7601  caucvgprlem2  7621  caucvgprprlem2  7651  suplocexprlemlub  7665  suplocexpr  7666  recexgt0sr  7714  archsr  7723  axpre-suploclemres  7842  conjmulap  8625  lerec2  8784  ledivp1  8798  cju  8856  nn2ge  8890  gtndiv  9286  supinfneg  9533  infsupneg  9534  z2ge  9762  iccssioo2  9882  fzrev3  10022  elfz1b  10025  exbtwnzlemstep  10183  exbtwnzlemex  10185  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnre  10192  flqdiv  10256  frec2uzled  10364  seq3caopr  10418  iseqf1olemab  10424  iseqf1olemnanb  10425  expnegzap  10489  nn0ltexp2  10623  hashen  10697  hashunlem  10717  hashprg  10721  leisorel  10750  zfz1isolemiso  10752  seq3coll  10755  caucvgrelemrec  10921  resqrexlemex  10967  minmax  11171  xrminmax  11206  fsum2dlemstep  11375  fisumcom2  11379  zproddc  11520  fprod2dlemstep  11563  fprodcom2fi  11567  zsupcllemstep  11878  zsupssdc  11887  bezoutlemmain  11931  sqgcd  11962  pcpremul  12225  pceulem  12226  pceu  12227  pczpre  12229  pcdiv  12234  pcqmul  12235  pcqdiv  12239  pcexp  12241  pcdvdsb  12251  pcneg  12256  pcdvdstr  12258  pcgcd1  12259  pc2dvds  12261  pcz  12263  pcaddlem  12270  pcadd  12271  qexpz  12282  expnprm  12283  infpnlem2  12290  neiint  12785  restbasg  12808  iscnp4  12858  cnconst2  12873  cnpdis  12882  neitx  12908  upxp  12912  hmeoimaf1o  12954  blssexps  13069  blssex  13070  ssblex  13071  bdmopn  13144  xmettx  13150  metcnp3  13151  tgioo  13186  tgqioo  13187  sin0pilem2  13343  logbgcd1irr  13525  lgsval  13545  lgsfcl2  13547  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  pwle2  13878