Theorem syl21anc 835

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 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl21anc.4	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
6	3, 4, 5	syl2anc 584	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  syl1111anc  837  wereu2  5587  frpomin  6247  funtpg  6496  funcnvtp  6504  funcnvqp  6505  fnund  6555  fun2d  6647  fvun1  6868  iinpreima  6955  ftpg  7037  fsnunf  7066  f1prex  7165  soisores  7207  isotr  7216  off  7560  caofrss  7578  caonncan  7583  fvmpocurryd  8096  oaf1o  8403  omeulem1  8422  oeordi  8427  oelimcl  8440  oeeulem  8441  oeeui  8442  oaabs2  8488  omabs  8490  pmresg  8667  ralxpmap  8693  domunsncan  8868  sucdom2OLD  8878  sucdom2  8998  unxpdom2  9040  sucxpdom  9041  unblem4  9078  fodomfi  9101  hartogslem1  9310  cantnflt  9439  cantnflem3  9458  cantnflem4  9459  cnfcomlem  9466  cnfcom  9467  ttrcltr  9483  infxpenlem  9778  infxpenc  9783  fseqenlem1  9789  pwsdompw  9969  cfeq0  10021  cofsmo  10034  cfsmolem  10035  ssfin4  10075  hsmexlem4  10194  hsmexlem5  10195  axdc3lem2  10216  fpwwe2  10408  wunpr  10474  mulclpi  10658  mulcanenq  10725  distrlem4pr  10791  prlem934  10798  prlem936  10812  divge0d  12821  elfznelfzob  13502  seqcaopr2  13768  facavg  14024  swrdwrdsymb  14384  cats1un  14443  f1oun2prg  14639  sqrtdiv  14986  sqrtdivd  15144  mulcn2  15314  o1of2  15331  fsumsplit  15462  sumsplit  15489  isumless  15566  demoivreALT  15919  rpnnen2lem11  15942  gcdnncl  16223  qredeu  16372  rpdvds  16374  isprm5  16421  rpexp  16436  divnumden  16461  divdenle  16462  phimullem  16489  phisum  16500  pythagtriplem4  16529  pythagtriplem8  16533  pythagtriplem9  16534  pcgcd1  16587  sumhash  16606  fldivp1  16607  pockthlem  16615  setsfun  16881  setsfun0  16882  ssc2  17543  estrreslem1  17862  estrreslem1OLD  17863  tleile  18148  mndpropd  18419  grpidssd  18660  grpinvssd  18661  issubg2  18779  isnsg3  18797  eqgid  18817  gass  18916  symgextres  19042  gsmsymgreqlem2  19048  sylow1lem5  19216  sylow2alem2  19232  sylow3lem3  19243  efgredlemd  19359  efgredlem  19362  frgpnabllem1  19483  frgpnabllem2  19484  subgdmdprd  19646  ablfacrplem  19677  kerf1ghm  19996  issrngd  20130  lmodprop2d  20194  lsspropd  20288  pwssplit1  20330  lspvadd  20367  znidomb  20778  znrrg  20782  lindfind  21032  lindsind  21033  mplsubglem  21214  mplind  21287  mat1ghm  21641  mdetunilem1  21770  mdetunilem3  21772  mdetunilem4  21773  mdetunilem9  21778  cramerimplem2  21842  mat2pmatlin  21893  monmatcollpw  21937  cpmadugsumlemF  22034  mretopd  22252  neiptopnei  22292  neitr  22340  ufilen  23090  flimrest  23143  flimclslem  23144  fclsrest  23184  cnextcn  23227  haustsms2  23297  tsmsxplem2  23314  trust  23390  utoptop  23395  restutop  23398  ustuqtop4  23405  utopsnneiplem  23408  utop2nei  23411  utop3cls  23412  isucn2  23440  ucncn  23446  fmucnd  23453  trcfilu  23455  comet  23678  metustexhalf  23721  metustbl  23731  psmetutop  23732  nrmmetd  23739  reconnlem1  23998  reconnlem2  23999  fsumcn  24042  cmetcaulem  24461  iscmet3lem1  24464  iscmet3lem2  24465  bcthlem5  24501  cmslsschl  24550  rrxdstprj1  24582  minveclem4  24605  ovolfiniun  24674  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  itgsplitioo  25011  c1liplem1  25169  dvfsumlem1  25199  plyeq0lem  25380  quotcan  25478  psercnlem1  25593  cxplea  25860  birthdaylem3  26112  musumsum  26350  dvdsmulf1o  26352  dchrelbas4  26400  dchrhash  26428  gausslemma2dlem0d  26516  gausslemma2dlem1a  26522  2lgslem1a1  26546  2sqlem8a  26582  2sqlem8  26583  2sqcoprm  26592  2sqmod  26593  chto1ub  26633  vmadivsum  26639  dchrisumlem1  26646  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  rpvmasum2  26669  mulog2sumlem2  26692  selberg2lem  26707  pntrmax  26721  pntpbnd1  26743  pntlemb  26754  pntlemj  26760  tgjustc1  26845  tgjustc2  26846  ercgrg  26887  motcgr  26906  tglineeltr  27001  colline  27019  miriso  27040  midexlem  27062  perpneq  27084  foot  27092  f1otrg  27241  axcontlem9  27349  uspgr1ewop  27624  nbupgrres  27740  structtocusgr  27822  wlkp1  28058  clwlkl1loop  28160  uspgrn2crct  28182  crctcshwlkn0lem5  28188  3trlond  28546  3pthond  28548  3spthond  28550  frgr3v  28648  vdgn1frgrv2  28669  numclwwlk3  28758  nmblolbii  29170  minvecolem3  29247  minvecolem4  29251  htthlem  29288  bcs2  29553  nmopub2tALT  30280  nmfnleub2  30297  eighmorth  30335  nmophmi  30402  nmopcoadji  30472  hstle  30601  atcvat3i  30767  opreu2reuALT  30834  iinabrex  30917  disjxpin  30936  fmptco1f1o  30977  off2  30987  xppreima2  30997  fgreu  31018  suppovss  31026  1stpreimas  31047  padct  31063  resf1o  31074  fpwrelmap  31077  xrofsup  31099  eliccelico  31107  elicoelioo  31108  iocinif  31111  difioo  31112  prmdvdsbc  31139  ccatf1  31232  pfxlsw2ccat  31233  wrdt2ind  31234  ressprs  31250  xrge0addgt0  31309  xrge0adddir  31310  gsumhashmul  31325  omndmul3  31348  gsumle  31359  symgcom  31361  pmtrcnel  31367  pmtrcnel2  31368  pmtrcnelor  31369  cycpmfv2  31390  trsp2cyc  31399  cycpmco2lem7  31408  cyc3genpm  31428  cycpmconjslem2  31431  cyc3conja  31433  archirng  31451  archirngz  31452  orngmul  31511  linds2eq  31584  nsgqusf1olem3  31609  rhmpreimaidl  31612  elrspunidl  31615  isprmidlc  31632  qsidomlem1  31637  qsidomlem2  31638  lindsunlem  31714  lbsdiflsp0  31716  fedgmullem1  31719  fedgmullem2  31720  1smat1  31763  madjusmdetlem2  31787  qtophaus  31795  locfinref  31800  zarclssn  31832  zar0ring  31837  zarmxt1  31839  rhmpreimacnlem  31843  rhmpreimacn  31844  metideq  31852  sqsscirc2  31868  tpr2rico  31871  fmcncfil  31890  lmxrge0  31911  lmdvg  31912  qqhval2lem  31940  qqhf  31945  qqhnm  31949  esumle  32035  gsumesum  32036  esumlef  32039  esumrnmpt2  32045  esumpcvgval  32055  esum2d  32070  ofcf  32080  ldsysgenld  32137  ldgenpisyslem1  32140  unelros  32148  difelros  32149  inelsros  32155  diffiunisros  32156  imambfm  32238  omssubadd  32276  inelcarsg  32287  carsgsigalem  32291  carsggect  32294  carsgclctunlem2  32295  oddpwdc  32330  eulerpartlems  32336  eulerpartlemb  32344  eulerpartlemt  32347  iwrdsplit  32363  sseqf  32368  sseqfres  32369  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemfrcn0  32505  sgnsub  32520  plymulx0  32535  signsplypnf  32538  signsvtn0  32558  signstfvneq0  32560  signsvtp  32571  signsvtn  32572  fsum2dsub  32596  reprlt  32608  hashreprin  32609  reprgt  32610  reprpmtf1o  32615  chtvalz  32618  breprexplema  32619  breprexplemc  32621  breprexp  32622  circlemeth  32629  logdivsqrle  32639  hgt750lemb  32645  lpadlem3  32667  lpadleft  32672  bnj1536  32843  bnj1001  32948  bnj1280  33009  cvxsconn  33214  satffunlem1  33378  satffunlem2  33379  elmrsubrn  33491  noextend  33878  neibastop3  34560  finxpsuclem  35577  poimirlem16  35802  poimirlem19  35805  poimirlem20  35806  poimirlem29  35815  mblfinlem3  35825  itg2addnclem3  35839  ftc1cnnclem  35857  lautlt  38112  lautcvr  38113  lauteq  38116  lautco  38118  ltrncl  38146  ltrncnvleN  38151  trljat2  38188  cdlemc6  38217  cdleme20c  38332  cdleme20j  38339  cdleme22e  38365  cdleme22eALTN  38366  cdlemg7aN  38646  cdlemg12e  38668  cdlemg17dALTN  38685  cdlemh  38838  cdlemkfid1N  38942  dibglbN  39187  diblss  39191  diclspsn  39215  dih1  39307  dihglbcpreN  39321  dihmeetlem4preN  39327  lcfrlem19  39582  aks4d1p8d1  40099  fsuppind  40286  mapfzcons  40545  mzpcl34  40560  mzpindd  40575  mzpsubst  40577  diophrw  40588  diophren  40642  irrapxlem1  40651  pellexlem5  40662  acongrep  40809  pwssplit4  40921  omssrncard  41154  brtrclfv2  41342  rfovcnvf1od  41619  ntrk0kbimka  41656  isotone1  41665  isotone2  41666  4an4132  42126  mulltgt0  42572  fnchoice  42579  3adantlr3  42591  3adantll2  42593  3adantll3  42594  uzwo4  42608  disjf1o  42736  supxrgelem  42883  infleinflem2  42917  xrralrecnnle  42929  supxrunb3  42946  unb2ltle  42962  infrpgernmpt  43012  iooiinicc  43087  iooiinioc  43101  fmuldfeq  43131  mccl  43146  limccog  43168  limcrecl  43177  lptioo1  43180  islpcn  43187  limsupre  43189  neglimc  43195  0ellimcdiv  43197  limclner  43199  climleltrp  43224  climinf3  43264  liminflimsupclim  43355  xlimpnfxnegmnf  43362  icccncfext  43435  fprodcncf  43448  dvnmptdivc  43486  dvnmul  43491  dvmptfprod  43493  dvnprodlem3  43496  stoweidlem25  43573  stoweidlem34  43582  stoweidlem38  43586  stoweidlem44  43592  stoweidlem48  43596  stoweidlem49  43597  stoweidlem59  43607  stoweidlem60  43608  wallispilem4  43616  stirlinglem5  43626  dirkercncflem2  43652  fourierdlem39  43694  fourierdlem42  43697  fourierdlem46  43700  fourierdlem47  43701  fourierdlem48  43702  fourierdlem50  43704  fourierdlem51  43705  fourierdlem64  43718  fourierdlem73  43727  fourierdlem74  43728  fourierdlem77  43731  fourierdlem80  43734  fourierdlem87  43741  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  etransclem32  43814  rrxsnicc  43848  sge0cl  43926  sge0f1o  43927  nnfoctbdjlem  44000  ismeannd  44012  omeiunltfirp  44064  hoicvr  44093  ovncvrrp  44109  hoidmvlelem2  44141  hoidmvlelem5  44144  hspdifhsp  44161  hoiqssbllem2  44168  hspmbllem2  44172  vonicclem2  44229  smflimsuplem7  44370  fundcmpsurbijinj  44873  sqrtpwpw2p  45001  isomgrref  45298  lincresunit2  45830  nnpw2pmod  45940  dignn0flhalflem1  45972  dignn0flhalf  45975  rrx2linest  46099  itsclc0yqsol  46121  itsclc0b  46129  functhinclem1  46333  functhinclem2  46334  fullthinc2  46339