Theorem syl12anc 1272

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  1275  cocan1  5966  fliftfun  5975  isopolem  6001  f1oiso2  6006  caovcld  6216  caovcomd  6219  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  1dom1el  7073  fidceq  7137  findcard2d  7161  diffifi  7164  tridc  7170  en2eqpr  7180  sbthlemi9  7248  supisolem  7312  ordiso2  7339  difinfsnlem  7403  difinfsn  7404  pr2cv1  7505  prarloclemup  7826  prarloc  7834  nqprl  7882  nqpru  7883  ltaddpr  7928  aptiprlemu  7971  archpr  7974  cauappcvgprlem2  7991  caucvgprlem2  8011  caucvgprprlem2  8041  suplocexprlemlub  8055  suplocexpr  8056  recexgt0sr  8104  archsr  8113  axpre-suploclemres  8232  conjmulap  9020  lerec2  9180  ledivp1  9194  cju  9252  nn2ge  9287  gtndiv  9691  supinfneg  9945  infsupneg  9946  z2ge  10178  iccssioo2  10298  fzrev3  10443  elfz1b  10446  zsupcllemstep  10611  zsupssdc  10622  exbtwnzlemstep  10631  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnre  10640  flqdiv  10707  frec2uzled  10815  seq3caopr  10881  seqcaoprg  10882  iseqf1olemab  10888  iseqf1olemnanb  10889  seqf1oglem1  10905  expnegzap  10959  nn0ltexp2  11096  hashen  11172  hashunlem  11193  hashprg  11198  hashfibclem  11231  leisorel  11234  zfz1isolemiso  11236  seq3coll  11239  swrdccat3b  11457  caucvgrelemrec  11689  resqrexlemex  11735  minmax  11940  xrminmax  11975  fsum2dlemstep  12145  fisumcom2  12149  zproddc  12290  fprod2dlemstep  12333  fprodcom2fi  12337  bezoutlemmain  12719  sqgcd  12750  pcpremul  13016  pceulem  13017  pceu  13018  pczpre  13020  pcdiv  13025  pcqmul  13026  pcqdiv  13030  pcexp  13032  pcdvdsb  13043  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pc2dvds  13053  pcz  13055  pcaddlem  13062  pcadd  13063  qexpz  13075  expnprm  13076  infpnlem2  13083  ballotfilemfc0  13176  ballotfilemfcc  13177  f1ocpbllem  13574  f1ovscpbl  13576  sgrppropd  13676  mndpropd  13701  grpsubpropd2  13860  f1ghm0to0  14025  ablnnncan  14076  rngpropd  14194  ringpropd  14281  lmodprop2d  14622  lsspropdg  14705  neiint  15136  restbasg  15159  iscnp4  15209  cnconst2  15224  cnpdis  15233  neitx  15259  upxp  15263  hmeoimaf1o  15305  blssexps  15420  blssex  15421  ssblex  15422  bdmopn  15495  xmettx  15501  metcnp3  15502  tgioo  15545  tgqioo  15546  dvmptfsum  15716  elply2  15726  sin0pilem2  15773  logbgcd1irr  15958  perfect  15995  lgsval  16003  lgsfcl2  16005  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  clwwlknonex2e  16561  pwle2  16898  qdiff  16959