Theorem syl12anc 1276

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  syl22anc  1279  cocan1  5993  fliftfun  6002  isopolem  6028  f1oiso2  6033  caovcld  6243  caovcomd  6246  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  1dom1el  7107  fidceq  7171  findcard2d  7195  diffifi  7198  tridc  7204  en2eqpr  7214  sbthlemi9  7282  supisolem  7349  ordiso2  7376  difinfsnlem  7440  difinfsn  7441  pr2cv1  7542  prarloclemup  7863  prarloc  7871  nqprl  7919  nqpru  7920  ltaddpr  7965  aptiprlemu  8008  archpr  8011  cauappcvgprlem2  8028  caucvgprlem2  8048  caucvgprprlem2  8078  suplocexprlemlub  8092  suplocexpr  8093  recexgt0sr  8141  archsr  8150  axpre-suploclemres  8269  conjmulap  9062  lerec2  9222  ledivp1  9236  cju  9294  nn2ge  9340  gtndiv  9746  supinfneg  10005  infsupneg  10006  z2ge  10239  iccssioo2  10359  fzrev3  10505  elfz1b  10508  zsupcllemstep  10673  zsupssdc  10684  exbtwnzlemstep  10693  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnre  10702  flqdiv  10773  frec2uzled  10881  seq3caopr  10947  seqcaoprg  10948  iseqf1olemab  10954  iseqf1olemnanb  10955  seqf1oglem1  10971  expnegzap  11025  nn0ltexp2  11163  hashen  11239  hashunlem  11260  hashprg  11265  hashfibclem  11298  hashf1lem2  11302  leisorel  11305  zfz1isolemiso  11307  seq3coll  11310  swrdccat3b  11528  caucvgrelemrec  11761  resqrexlemex  11807  minmax  12014  xrminmax  12050  fsum2dlemstep  12220  fisumcom2  12224  zproddc  12365  fprod2dlemstep  12408  fprodcom2fi  12412  bezoutlemmain  12794  sqgcd  12825  pcpremul  13095  pceulem  13096  pceu  13097  pczpre  13099  pcdiv  13104  pcqmul  13105  pcqdiv  13109  pcexp  13111  pcdvdsb  13122  pcneg  13127  pcdvdstr  13129  pcgcd1  13130  pc2dvds  13132  pcz  13134  pcaddlem  13141  pcadd  13142  qexpz  13154  expnprm  13155  infpnlem2  13162  ballotfilemfc0  13284  ballotfilemfcc  13285  f1ocpbllem  13684  f1ovscpbl  13686  sgrppropd  13781  mndpropd  13806  grpsubpropd2  13963  f1ghm0to0  14128  ablnnncan  14211  rngpropd  14338  ringpropd  14427  lmodprop2d  14769  lsspropdg  14852  assapropd  15098  neiint  15337  restbasg  15360  iscnp4  15410  cnconst2  15425  cnpdis  15434  neitx  15460  upxp  15464  hmeoimaf1o  15506  blssexps  15621  blssex  15622  ssblex  15623  bdmopn  15696  xmettx  15702  metcnp3  15703  tgioo  15746  tgqioo  15747  dvmptfsum  15917  elply2  15927  sin0pilem2  15975  logbgcd1irr  16164  perfect  16262  bposlem2  16273  lgsval  16289  lgsfcl2  16291  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  clwwlknonex2e  16847  pwle2  17194  qdiff  17265