Theorem syl21anc 834

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 583	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 206  df-an 396

This theorem is referenced by:  syl1111anc  836  wereu2  5577  frpomin  6228  funtpg  6473  funcnvtp  6481  funcnvqp  6482  fnund  6530  fun2d  6622  fvun1  6841  iinpreima  6928  ftpg  7010  fsnunf  7039  f1prex  7136  soisores  7178  isotr  7187  off  7529  caofrss  7547  caonncan  7552  fvmpocurryd  8058  oaf1o  8356  omeulem1  8375  oeordi  8380  oelimcl  8393  oeeulem  8394  oeeui  8395  oaabs2  8439  omabs  8441  pmresg  8616  ralxpmap  8642  domunsncan  8812  sucdom2  8822  unxpdom2  8960  sucxpdom  8961  unblem4  8999  fodomfi  9022  hartogslem1  9231  cantnflt  9360  cantnflem3  9379  cantnflem4  9380  cnfcomlem  9387  cnfcom  9388  infxpenlem  9700  infxpenc  9705  fseqenlem1  9711  pwsdompw  9891  cfeq0  9943  cofsmo  9956  cfsmolem  9957  ssfin4  9997  hsmexlem4  10116  hsmexlem5  10117  axdc3lem2  10138  fpwwe2  10330  wunpr  10396  mulclpi  10580  mulcanenq  10647  distrlem4pr  10713  prlem934  10720  prlem936  10734  divge0d  12741  elfznelfzob  13421  seqcaopr2  13687  facavg  13943  swrdwrdsymb  14303  cats1un  14362  f1oun2prg  14558  sqrtdiv  14905  sqrtdivd  15063  mulcn2  15233  o1of2  15250  fsumsplit  15381  sumsplit  15408  isumless  15485  demoivreALT  15838  rpnnen2lem11  15861  gcdnncl  16142  qredeu  16291  rpdvds  16293  isprm5  16340  rpexp  16355  divnumden  16380  divdenle  16381  phimullem  16408  phisum  16419  pythagtriplem4  16448  pythagtriplem8  16452  pythagtriplem9  16453  pcgcd1  16506  sumhash  16525  fldivp1  16526  pockthlem  16534  setsfun  16800  setsfun0  16801  ssc2  17451  estrreslem1  17769  estrreslem1OLD  17770  tleile  18054  mndpropd  18325  grpidssd  18566  grpinvssd  18567  issubg2  18685  isnsg3  18703  eqgid  18723  gass  18822  symgextres  18948  gsmsymgreqlem2  18954  sylow1lem5  19122  sylow2alem2  19138  sylow3lem3  19149  efgredlemd  19265  efgredlem  19268  frgpnabllem1  19389  frgpnabllem2  19390  subgdmdprd  19552  ablfacrplem  19583  kerf1ghm  19902  issrngd  20036  lmodprop2d  20100  lsspropd  20194  pwssplit1  20236  lspvadd  20273  znidomb  20681  znrrg  20685  lindfind  20933  lindsind  20934  mplsubglem  21115  mplind  21188  mat1ghm  21540  mdetunilem1  21669  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  cramerimplem2  21741  mat2pmatlin  21792  monmatcollpw  21836  cpmadugsumlemF  21933  mretopd  22151  neiptopnei  22191  neitr  22239  ufilen  22989  flimrest  23042  flimclslem  23043  fclsrest  23083  cnextcn  23126  haustsms2  23196  tsmsxplem2  23213  trust  23289  utoptop  23294  restutop  23297  ustuqtop4  23304  utopsnneiplem  23307  utop2nei  23310  utop3cls  23311  isucn2  23339  ucncn  23345  fmucnd  23352  trcfilu  23354  comet  23575  metustexhalf  23618  metustbl  23628  psmetutop  23629  nrmmetd  23636  reconnlem1  23895  reconnlem2  23896  fsumcn  23939  cmetcaulem  24357  iscmet3lem1  24360  iscmet3lem2  24361  bcthlem5  24397  cmslsschl  24446  rrxdstprj1  24478  minveclem4  24501  ovolfiniun  24570  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  itgsplitioo  24907  c1liplem1  25065  dvfsumlem1  25095  plyeq0lem  25276  quotcan  25374  psercnlem1  25489  cxplea  25756  birthdaylem3  26008  musumsum  26246  dvdsmulf1o  26248  dchrelbas4  26296  dchrhash  26324  gausslemma2dlem0d  26412  gausslemma2dlem1a  26418  2lgslem1a1  26442  2sqlem8a  26478  2sqlem8  26479  2sqcoprm  26488  2sqmod  26489  chto1ub  26529  vmadivsum  26535  dchrisumlem1  26542  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  rpvmasum2  26565  mulog2sumlem2  26588  selberg2lem  26603  pntrmax  26617  pntpbnd1  26639  pntlemb  26650  pntlemj  26656  tgjustc1  26740  tgjustc2  26741  ercgrg  26782  motcgr  26801  tglineeltr  26896  colline  26914  miriso  26935  midexlem  26957  perpneq  26979  foot  26987  f1otrg  27136  axcontlem9  27243  uspgr1ewop  27518  nbupgrres  27634  structtocusgr  27716  wlkp1  27951  clwlkl1loop  28052  uspgrn2crct  28074  crctcshwlkn0lem5  28080  3trlond  28438  3pthond  28440  3spthond  28442  frgr3v  28540  vdgn1frgrv2  28561  numclwwlk3  28650  nmblolbii  29062  minvecolem3  29139  minvecolem4  29143  htthlem  29180  bcs2  29445  nmopub2tALT  30172  nmfnleub2  30189  eighmorth  30227  nmophmi  30294  nmopcoadji  30364  hstle  30493  atcvat3i  30659  opreu2reuALT  30726  iinabrex  30809  disjxpin  30828  fmptco1f1o  30869  off2  30879  xppreima2  30889  fgreu  30911  suppovss  30919  1stpreimas  30940  padct  30956  resf1o  30967  fpwrelmap  30970  xrofsup  30992  eliccelico  31000  elicoelioo  31001  iocinif  31004  difioo  31005  prmdvdsbc  31032  ccatf1  31125  pfxlsw2ccat  31126  wrdt2ind  31127  ressprs  31143  xrge0addgt0  31202  xrge0adddir  31203  gsumhashmul  31218  omndmul3  31241  gsumle  31252  symgcom  31254  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  cycpmfv2  31283  trsp2cyc  31292  cycpmco2lem7  31301  cyc3genpm  31321  cycpmconjslem2  31324  cyc3conja  31326  archirng  31344  archirngz  31345  orngmul  31404  linds2eq  31477  nsgqusf1olem3  31502  rhmpreimaidl  31505  elrspunidl  31508  isprmidlc  31525  qsidomlem1  31530  qsidomlem2  31531  lindsunlem  31607  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  1smat1  31656  madjusmdetlem2  31680  qtophaus  31688  locfinref  31693  zarclssn  31725  zar0ring  31730  zarmxt1  31732  rhmpreimacnlem  31736  rhmpreimacn  31737  metideq  31745  sqsscirc2  31761  tpr2rico  31764  fmcncfil  31783  lmxrge0  31804  lmdvg  31805  qqhval2lem  31831  qqhf  31836  qqhnm  31840  esumle  31926  gsumesum  31927  esumlef  31930  esumrnmpt2  31936  esumpcvgval  31946  esum2d  31961  ofcf  31971  ldsysgenld  32028  ldgenpisyslem1  32031  unelros  32039  difelros  32040  inelsros  32046  diffiunisros  32047  imambfm  32129  omssubadd  32167  inelcarsg  32178  carsgsigalem  32182  carsggect  32185  carsgclctunlem2  32186  oddpwdc  32221  eulerpartlems  32227  eulerpartlemb  32235  eulerpartlemt  32238  iwrdsplit  32254  sseqf  32259  sseqfres  32260  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfrcn0  32396  sgnsub  32411  plymulx0  32426  signsplypnf  32429  signsvtn0  32449  signstfvneq0  32451  signsvtp  32462  signsvtn  32463  fsum2dsub  32487  reprlt  32499  hashreprin  32500  reprgt  32501  reprpmtf1o  32506  chtvalz  32509  breprexplema  32510  breprexplemc  32512  breprexp  32513  circlemeth  32520  logdivsqrle  32530  hgt750lemb  32536  lpadlem3  32558  lpadleft  32563  bnj1536  32734  bnj1001  32839  bnj1280  32900  cvxsconn  33105  satffunlem1  33269  satffunlem2  33270  elmrsubrn  33382  ttrcltr  33702  noextend  33796  neibastop3  34478  finxpsuclem  35495  poimirlem16  35720  poimirlem19  35723  poimirlem20  35724  poimirlem29  35733  mblfinlem3  35743  itg2addnclem3  35757  ftc1cnnclem  35775  lautlt  38032  lautcvr  38033  lauteq  38036  lautco  38038  ltrncl  38066  ltrncnvleN  38071  trljat2  38108  cdlemc6  38137  cdleme20c  38252  cdleme20j  38259  cdleme22e  38285  cdleme22eALTN  38286  cdlemg7aN  38566  cdlemg12e  38588  cdlemg17dALTN  38605  cdlemh  38758  cdlemkfid1N  38862  dibglbN  39107  diblss  39111  diclspsn  39135  dih1  39227  dihglbcpreN  39241  dihmeetlem4preN  39247  lcfrlem19  39502  aks4d1p8d1  40020  fsuppind  40202  mapfzcons  40454  mzpcl34  40469  mzpindd  40484  mzpsubst  40486  diophrw  40497  diophren  40551  irrapxlem1  40560  pellexlem5  40571  acongrep  40718  pwssplit4  40830  brtrclfv2  41224  rfovcnvf1od  41501  ntrk0kbimka  41538  isotone1  41547  isotone2  41548  4an4132  42008  mulltgt0  42454  fnchoice  42461  3adantlr3  42473  3adantll2  42475  3adantll3  42476  uzwo4  42490  disjf1o  42618  supxrgelem  42766  infleinflem2  42800  xrralrecnnle  42812  supxrunb3  42829  unb2ltle  42845  infrpgernmpt  42895  iooiinicc  42970  iooiinioc  42984  fmuldfeq  43014  mccl  43029  limccog  43051  limcrecl  43060  lptioo1  43063  islpcn  43070  limsupre  43072  neglimc  43078  0ellimcdiv  43080  limclner  43082  climleltrp  43107  climinf3  43147  liminflimsupclim  43238  xlimpnfxnegmnf  43245  icccncfext  43318  fprodcncf  43331  dvnmptdivc  43369  dvnmul  43374  dvmptfprod  43376  dvnprodlem3  43379  stoweidlem25  43456  stoweidlem34  43465  stoweidlem38  43469  stoweidlem44  43475  stoweidlem48  43479  stoweidlem49  43480  stoweidlem59  43490  stoweidlem60  43491  wallispilem4  43499  stirlinglem5  43509  dirkercncflem2  43535  fourierdlem39  43577  fourierdlem42  43580  fourierdlem46  43583  fourierdlem47  43584  fourierdlem48  43585  fourierdlem50  43587  fourierdlem51  43588  fourierdlem64  43601  fourierdlem73  43610  fourierdlem74  43611  fourierdlem77  43614  fourierdlem80  43617  fourierdlem87  43624  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  etransclem32  43697  rrxsnicc  43731  sge0cl  43809  sge0f1o  43810  nnfoctbdjlem  43883  ismeannd  43895  omeiunltfirp  43947  hoicvr  43976  ovncvrrp  43992  hoidmvlelem2  44024  hoidmvlelem5  44027  hspdifhsp  44044  hoiqssbllem2  44051  hspmbllem2  44055  vonicclem2  44112  smflimsuplem7  44246  fundcmpsurbijinj  44750  sqrtpwpw2p  44878  isomgrref  45175  lincresunit2  45707  nnpw2pmod  45817  dignn0flhalflem1  45849  dignn0flhalf  45852  rrx2linest  45976  itsclc0yqsol  45998  itsclc0b  46006  functhinclem1  46210  functhinclem2  46211  fullthinc2  46216