Theorem syl21anc 838

Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl21anc.4	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl21anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	3, 4, 5	syl2anc 585	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  bibiad  840  syl1111anc  841  rspc2dv  3579  wereu2  5628  frpomin  6304  funtpg  6553  funcnvtp  6561  funcnvqp  6562  fnund  6613  fun2d  6704  fvun1  6931  iinpreima  7021  ftpg  7110  fsnunf  7140  f1prex  7239  soisores  7282  isotr  7291  off  7649  coof  7655  caofrss  7670  caonncan  7675  fvmpocurryd  8221  oaf1o  8498  omeulem1  8517  oeordi  8523  oelimcl  8536  oeeulem  8537  oeeui  8538  oaabs2  8585  omabs  8587  coflton  8607  pmresg  8818  ralxpmap  8844  domunsncan  9015  sucdom2  9137  unxpdom2  9170  sucxpdom  9171  unblem4  9205  fodomfi  9222  fodomfiOLD  9240  hartogslem1  9457  cantnflt  9593  cantnflem3  9612  cantnflem4  9613  cnfcomlem  9620  cnfcom  9621  ttrcltr  9637  infxpenlem  9935  infxpenc  9940  fseqenlem1  9946  pwsdompw  10125  cfeq0  10178  cofsmo  10191  cfsmolem  10192  ssfin4  10232  hsmexlem4  10351  hsmexlem5  10352  axdc3lem2  10373  fpwwe2  10566  wunpr  10632  mulclpi  10816  mulcanenq  10883  distrlem4pr  10949  prlem934  10956  prlem936  10970  divge0d  13026  elfzodif0  13725  elfznelfzob  13729  seqcaopr2  14000  facavg  14263  swrdwrdsymb  14625  cats1un  14683  f1oun2prg  14879  sqrtdiv  15227  sqrtdivd  15386  mulcn2  15558  o1of2  15575  fsumsplit  15703  sumsplit  15730  isumless  15810  demoivreALT  16168  rpnnen2lem11  16191  gcdnncl  16476  qredeu  16627  rpdvds  16629  isprm5  16677  rpexp  16692  prmdvdsbc  16696  divnumden  16718  divdenle  16719  phimullem  16749  phisum  16761  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  pcgcd1  16848  sumhash  16867  fldivp1  16868  pockthlem  16876  setsfun  17141  setsfun0  17142  ssc2  17789  estrreslem1  18103  tleile  18385  chnind  18587  sgrppropd  18699  mndpropd  18727  grpidssd  18992  grpinvssd  18993  issubg2  19117  isnsg3  19135  eqgid  19155  kerf1ghm  19222  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmqusker  19262  gass  19276  symgextres  19400  gsmsymgreqlem2  19406  sylow1lem5  19577  sylow2alem2  19593  sylow3lem3  19604  efgredlemd  19719  efgredlem  19722  frgpnabllem1  19848  frgpnabllem2  19849  subgdmdprd  20011  ablfacrplem  20042  omndmul3  20109  gsumle  20120  rglcom4d  20192  issrngd  20832  orngmul  20842  lmodprop2d  20919  lsspropd  21012  pwssplit1  21054  lspvadd  21091  rhmpreimaidl  21275  znidomb  21541  znrrg  21545  lindfind  21796  lindsind  21797  mplsubglem  21977  mplind  22048  evlsvvval  22071  ressply1evl  22335  mat1ghm  22448  mdetunilem1  22577  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  cramerimplem2  22649  mat2pmatlin  22700  monmatcollpw  22744  cpmadugsumlemF  22841  mretopd  23057  neiptopnei  23097  neitr  23145  ufilen  23895  flimrest  23948  flimclslem  23949  fclsrest  23989  cnextcn  24032  haustsms2  24102  tsmsxplem2  24119  trust  24194  utoptop  24199  restutop  24202  ustuqtop4  24209  utopsnneiplem  24212  utop2nei  24215  utop3cls  24216  isucn2  24243  ucncn  24249  fmucnd  24256  trcfilu  24258  comet  24478  metustexhalf  24521  metustbl  24531  psmetutop  24532  nrmmetd  24539  reconnlem1  24792  reconnlem2  24793  fsumcn  24837  cmetcaulem  25255  iscmet3lem1  25258  iscmet3lem2  25259  bcthlem5  25295  cmslsschl  25344  rrxdstprj1  25376  minveclem4  25399  ovolfiniun  25468  itg1addlem4  25666  itg1addlem5  25667  itgsplitioo  25805  c1liplem1  25963  dvfsumlem1  25993  plyeq0lem  26175  quotcan  26275  psercnlem1  26390  cxplea  26660  birthdaylem3  26917  musumsum  27155  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrelbas4  27206  dchrhash  27234  gausslemma2dlem0d  27322  gausslemma2dlem1a  27328  2lgslem1a1  27352  2sqlem8a  27388  2sqlem8  27389  2sqcoprm  27398  2sqmod  27399  chto1ub  27439  vmadivsum  27445  dchrisumlem1  27452  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  rpvmasum2  27475  mulog2sumlem2  27498  selberg2lem  27513  pntrmax  27527  pntpbnd1  27549  pntlemb  27560  pntlemj  27566  noextend  27630  cuteq0  27807  tgjustc1  28543  tgjustc2  28544  ercgrg  28585  motcgr  28604  tglineeltr  28699  colline  28717  miriso  28738  midexlem  28760  perpneq  28782  foot  28790  f1otrg  28939  axcontlem9  29041  uspgr1ewop  29317  nbupgrres  29433  structtocusgr  29515  wlkp1  29748  clwlkl1loop  29851  uspgrn2crct  29876  crctcshwlkn0lem5  29882  3trlond  30243  3pthond  30245  3spthond  30247  frgr3v  30345  vdgn1frgrv2  30366  numclwwlk3  30455  nmblolbii  30870  minvecolem3  30947  minvecolem4  30951  htthlem  30988  bcs2  31253  nmopub2tALT  31980  nmfnleub2  31997  eighmorth  32035  nmophmi  32102  nmopcoadji  32172  hstle  32301  atcvat3i  32467  opreu2reuALT  32546  prssad  32599  prssbd  32600  iinabrex  32639  disjxpin  32658  fmptco1f1o  32706  off2  32714  xppreima2  32724  fgreu  32744  suppovss  32754  1stpreimas  32779  padct  32791  resf1o  32803  fpwrelmap  32806  arginv  32820  argcj  32821  xrofsup  32840  eliccelico  32850  elicoelioo  32851  iocinif  32854  difioo  32855  suppssnn0  32878  hashpss  32882  elq2  32885  sgnsub  32910  2exple2exp  32918  oexpled  32920  indsupp  32927  indfsid  32929  ccatf1  33009  pfxlsw2ccat  33010  wrdt2ind  33013  ressprs  33026  xrge0addgt0  33077  xrge0adddir  33078  mndlactf1o  33090  mndractf1o  33091  gsumhashmul  33128  gsummulsubdishift1  33129  symgcom  33144  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  cycpmfv2  33175  trsp2cyc  33184  cycpmco2lem7  33193  cyc3genpm  33213  cycpmconjslem2  33216  cyc3conja  33218  archirng  33249  archirngz  33250  rlocf1  33334  rrgsubm  33345  fracerl  33367  idomsubr  33370  linds2eq  33441  nsgqusf1olem3  33475  lidlunitel  33483  unitpidl1  33484  elrspunidl  33488  drngidl  33493  isprmidlc  33507  qsidomlem1  33512  qsidomlem2  33513  qsnzr  33515  mxidlirredi  33531  mxidlirred  33532  qsdrngi  33555  qsdrnglem2  33556  rprmasso  33585  1arithidomlem2  33596  1arithufdlem4  33607  zringidom  33611  deg1le0eq0  33633  ply1unit  33635  ply1dg1rt  33640  ply1dg3rt0irred  33644  m1pmeq  33645  evlextv  33686  mplvrpmrhm  33691  esplympl  33711  esplysply  33715  esplyind  33719  esplyindfv  33720  vietadeg1  33722  ply1degltdimlem  33766  ply1degltdim  33767  lindsunlem  33768  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  assalactf1o  33779  ply1annprmidl  33851  minplyirredlem  33854  irngnminplynz  33856  minplyelirng  33859  algextdeglem4  33864  constrconj  33889  constrsqrtcl  33923  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpinconstrlem1  33933  1smat1  33948  madjusmdetlem2  33972  qtophaus  33980  locfinref  33985  zarclssn  34017  zar0ring  34022  zarmxt1  34024  rhmpreimacnlem  34028  rhmpreimacn  34029  metideq  34037  sqsscirc2  34053  tpr2rico  34056  fmcncfil  34075  lmxrge0  34096  lmdvg  34097  qqhval2lem  34125  qqhf  34130  qqhnm  34134  esumle  34202  gsumesum  34203  esumlef  34206  esumrnmpt2  34212  esumpcvgval  34222  esum2d  34237  ofcf  34247  ldsysgenld  34304  ldgenpisyslem1  34307  unelros  34315  difelros  34316  inelsros  34322  diffiunisros  34323  imambfm  34406  omssubadd  34444  inelcarsg  34455  carsgsigalem  34459  carsggect  34462  carsgclctunlem2  34463  oddpwdc  34498  eulerpartlems  34504  eulerpartlemb  34512  eulerpartlemt  34515  iwrdsplit  34531  sseqf  34536  sseqfres  34537  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemfrcn0  34674  plymulx0  34691  signsplypnf  34694  signsvtn0  34714  signstfvneq0  34716  signsvtp  34727  signsvtn  34728  fsum2dsub  34751  reprlt  34763  hashreprin  34764  reprgt  34765  reprpmtf1o  34770  chtvalz  34773  breprexplema  34774  breprexplemc  34776  breprexp  34777  circlemeth  34784  logdivsqrle  34794  hgt750lemb  34800  lpadlem3  34822  lpadleft  34827  bnj1536  34996  bnj1001  35101  bnj1280  35162  fineqvnttrclselem2  35266  satffunlem1  35589  satffunlem2  35590  elmrsubrn  35702  neibastop3  36544  finxpsuclem  37713  poimirlem16  37957  poimirlem19  37960  poimirlem20  37961  poimirlem29  37970  mblfinlem3  37980  itg2addnclem3  37994  ftc1cnnclem  38012  lautlt  40537  lautcvr  40538  lauteq  40541  lautco  40543  ltrncl  40571  ltrncnvleN  40576  trljat2  40613  cdlemc6  40642  cdleme20c  40757  cdleme20j  40764  cdleme22e  40790  cdleme22eALTN  40791  cdlemg7aN  41071  cdlemg12e  41093  cdlemg17dALTN  41110  cdlemh  41263  cdlemkfid1N  41367  dibglbN  41612  diblss  41616  diclspsn  41640  dih1  41732  dihglbcpreN  41746  dihmeetlem4preN  41752  lcfrlem19  42007  aks4d1p8d1  42523  fsuppind  43023  mapfzcons  43148  mzpcl34  43163  mzpindd  43178  mzpsubst  43180  diophrw  43191  diophren  43241  irrapxlem1  43250  pellexlem5  43261  acongrep  43408  pwssplit4  43517  omlimcl2  43670  onexoegt  43672  oasubex  43714  omlim2  43727  nnoeomeqom  43740  nnawordexg  43755  succlg  43756  oacl2g  43758  onmcl  43759  omabs2  43760  omcl2  43761  tfsconcatrev  43776  ofoafg  43782  ofoaf  43783  ofoaass  43788  naddcnfass  43797  naddwordnexlem4  43829  omssrncard  43967  brtrclfv2  44154  rfovcnvf1od  44431  ntrk0kbimka  44466  isotone1  44475  isotone2  44476  4an4132  44926  modelaxrep  45408  mulltgt0  45453  fnchoice  45460  3adantlr3  45471  3adantll2  45472  3adantll3  45473  uzwo4  45484  disjf1o  45621  supxrgelem  45767  infleinflem2  45800  xrralrecnnle  45812  supxrunb3  45828  unb2ltle  45843  infrpgernmpt  45893  iooiinicc  45972  iooiinioc  45986  fmuldfeq  46013  mccl  46028  limccog  46050  limcrecl  46059  lptioo1  46062  islpcn  46067  limsupre  46069  neglimc  46075  0ellimcdiv  46077  limclner  46079  climleltrp  46104  climinf3  46144  liminflimsupclim  46235  xlimpnfxnegmnf  46242  icccncfext  46315  fprodcncf  46328  dvnmptdivc  46366  dvnmul  46371  dvmptfprod  46373  dvnprodlem3  46376  stoweidlem25  46453  stoweidlem34  46462  stoweidlem38  46466  stoweidlem44  46472  stoweidlem48  46476  stoweidlem49  46477  stoweidlem59  46487  stoweidlem60  46488  wallispilem4  46496  stirlinglem5  46506  dirkercncflem2  46532  fourierdlem39  46574  fourierdlem42  46577  fourierdlem46  46580  fourierdlem47  46581  fourierdlem48  46582  fourierdlem50  46584  fourierdlem51  46585  fourierdlem64  46598  fourierdlem73  46607  fourierdlem74  46608  fourierdlem77  46611  fourierdlem80  46614  fourierdlem87  46621  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  etransclem32  46694  rrxsnicc  46728  sge0cl  46809  sge0f1o  46810  nnfoctbdjlem  46883  ismeannd  46895  omeiunltfirp  46947  ovncvrrp  46992  hoidmvlelem2  47024  hoidmvlelem5  47027  hspdifhsp  47044  hoiqssbllem2  47051  hspmbllem2  47055  vonicclem2  47112  smflimsuplem7  47254  fundcmpsurbijinj  47870  sqrtpwpw2p  48001  lincresunit2  48954  nnpw2pmod  49059  dignn0flhalflem1  49091  dignn0flhalf  49094  rrx2linest  49218  itsclc0yqsol  49240  itsclc0b  49248  brab2dd  49303  oppcendc  49493  imaidfu  49585  imasubc  49626  oppcthinendcALT  49916  functhinclem1  49919  functhinclem2  49920  fullthinc2  49926