Theorem syl21anc 837

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 207  df-an 396

This theorem is referenced by:  syl1111anc  839  rspc2dv  3650  wereu2  5697  frpomin  6372  funtpg  6633  funcnvtp  6641  funcnvqp  6642  fnund  6694  fun2d  6785  fvun1  7013  iinpreima  7102  ftpg  7190  fsnunf  7219  f1prex  7320  soisores  7363  isotr  7372  off  7732  coof  7737  caofrss  7751  caonncan  7756  fvmpocurryd  8312  oaf1o  8619  omeulem1  8638  oeordi  8643  oelimcl  8656  oeeulem  8657  oeeui  8658  oaabs2  8705  omabs  8707  coflton  8727  pmresg  8928  ralxpmap  8954  domunsncan  9138  sucdom2OLD  9148  sucdom2  9269  unxpdom2  9317  sucxpdom  9318  unblem4  9359  fodomfi  9378  fodomfiOLD  9398  hartogslem1  9611  cantnflt  9741  cantnflem3  9760  cantnflem4  9761  cnfcomlem  9768  cnfcom  9769  ttrcltr  9785  infxpenlem  10082  infxpenc  10087  fseqenlem1  10093  pwsdompw  10272  cfeq0  10325  cofsmo  10338  cfsmolem  10339  ssfin4  10379  hsmexlem4  10498  hsmexlem5  10499  axdc3lem2  10520  fpwwe2  10712  wunpr  10778  mulclpi  10962  mulcanenq  11029  distrlem4pr  11095  prlem934  11102  prlem936  11116  divge0d  13139  elfznelfzob  13823  seqcaopr2  14089  facavg  14350  swrdwrdsymb  14710  cats1un  14769  f1oun2prg  14966  sqrtdiv  15314  sqrtdivd  15472  mulcn2  15642  o1of2  15659  fsumsplit  15789  sumsplit  15816  isumless  15893  demoivreALT  16249  rpnnen2lem11  16272  gcdnncl  16553  qredeu  16705  rpdvds  16707  isprm5  16754  rpexp  16769  prmdvdsbc  16773  divnumden  16795  divdenle  16796  phimullem  16826  phisum  16837  pythagtriplem4  16866  pythagtriplem8  16870  pythagtriplem9  16871  pcgcd1  16924  sumhash  16943  fldivp1  16944  pockthlem  16952  setsfun  17218  setsfun0  17219  ssc2  17883  estrreslem1  18205  estrreslem1OLD  18206  tleile  18491  sgrppropd  18769  mndpropd  18797  grpidssd  19056  grpinvssd  19057  issubg2  19181  isnsg3  19200  eqgid  19220  kerf1ghm  19287  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  gass  19341  symgextres  19467  gsmsymgreqlem2  19473  sylow1lem5  19644  sylow2alem2  19660  sylow3lem3  19671  efgredlemd  19786  efgredlem  19789  frgpnabllem1  19915  frgpnabllem2  19916  subgdmdprd  20078  ablfacrplem  20109  rglcom4d  20238  issrngd  20878  lmodprop2d  20944  lsspropd  21039  pwssplit1  21081  lspvadd  21118  rhmpreimaidl  21310  znidomb  21603  znrrg  21607  lindfind  21859  lindsind  21860  mplsubglem  22042  mplind  22117  ressply1evl  22395  mat1ghm  22510  mdetunilem1  22639  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  cramerimplem2  22711  mat2pmatlin  22762  monmatcollpw  22806  cpmadugsumlemF  22903  mretopd  23121  neiptopnei  23161  neitr  23209  ufilen  23959  flimrest  24012  flimclslem  24013  fclsrest  24053  cnextcn  24096  haustsms2  24166  tsmsxplem2  24183  trust  24259  utoptop  24264  restutop  24267  ustuqtop4  24274  utopsnneiplem  24277  utop2nei  24280  utop3cls  24281  isucn2  24309  ucncn  24315  fmucnd  24322  trcfilu  24324  comet  24547  metustexhalf  24590  metustbl  24600  psmetutop  24601  nrmmetd  24608  reconnlem1  24867  reconnlem2  24868  fsumcn  24913  cmetcaulem  25341  iscmet3lem1  25344  iscmet3lem2  25345  bcthlem5  25381  cmslsschl  25430  rrxdstprj1  25462  minveclem4  25485  ovolfiniun  25555  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  itgsplitioo  25893  c1liplem1  26055  dvfsumlem1  26086  plyeq0lem  26269  quotcan  26369  psercnlem1  26487  cxplea  26756  birthdaylem3  27014  musumsum  27253  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrelbas4  27305  dchrhash  27333  gausslemma2dlem0d  27421  gausslemma2dlem1a  27427  2lgslem1a1  27451  2sqlem8a  27487  2sqlem8  27488  2sqcoprm  27497  2sqmod  27498  chto1ub  27538  vmadivsum  27544  dchrisumlem1  27551  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  rpvmasum2  27574  mulog2sumlem2  27597  selberg2lem  27612  pntrmax  27626  pntpbnd1  27648  pntlemb  27659  pntlemj  27665  noextend  27729  cuteq0  27895  tgjustc1  28501  tgjustc2  28502  ercgrg  28543  motcgr  28562  tglineeltr  28657  colline  28675  miriso  28696  midexlem  28718  perpneq  28740  foot  28748  f1otrg  28897  axcontlem9  29005  uspgr1ewop  29283  nbupgrres  29399  structtocusgr  29481  wlkp1  29717  clwlkl1loop  29819  uspgrn2crct  29841  crctcshwlkn0lem5  29847  3trlond  30205  3pthond  30207  3spthond  30209  frgr3v  30307  vdgn1frgrv2  30328  numclwwlk3  30417  nmblolbii  30831  minvecolem3  30908  minvecolem4  30912  htthlem  30949  bcs2  31214  nmopub2tALT  31941  nmfnleub2  31958  eighmorth  31996  nmophmi  32063  nmopcoadji  32133  hstle  32262  atcvat3i  32428  bibiad  32486  opreu2reuALT  32505  iinabrex  32591  disjxpin  32610  fmptco1f1o  32652  off2  32660  xppreima2  32669  fgreu  32690  suppovss  32697  1stpreimas  32717  padct  32733  resf1o  32744  fpwrelmap  32747  xrofsup  32774  eliccelico  32782  elicoelioo  32783  iocinif  32786  difioo  32787  suppssnn0  32812  ccatf1  32915  pfxlsw2ccat  32917  wrdt2ind  32920  ressprs  32936  chnind  32983  xrge0addgt0  33003  xrge0adddir  33004  mndlactf1o  33016  mndractf1o  33017  gsumhashmul  33040  omndmul3  33063  gsumle  33074  symgcom  33076  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  cycpmfv2  33107  trsp2cyc  33116  cycpmco2lem7  33125  cyc3genpm  33145  cycpmconjslem2  33148  cyc3conja  33150  archirng  33168  archirngz  33169  rlocf1  33245  rrgsubm  33253  fracerl  33273  idomsubr  33276  orngmul  33298  linds2eq  33374  nsgqusf1olem3  33408  lidlunitel  33416  unitpidl1  33417  elrspunidl  33421  drngidl  33426  isprmidlc  33440  qsidomlem1  33445  qsidomlem2  33446  qsnzr  33448  mxidlirredi  33464  mxidlirred  33465  qsdrngi  33488  qsdrnglem2  33489  rprmasso  33518  1arithidomlem2  33529  1arithufdlem4  33540  zringidom  33544  deg1le0eq0  33563  ply1unit  33565  ply1dg1rt  33569  ply1dg3rt0irred  33572  m1pmeq  33573  ply1degltdimlem  33635  ply1degltdim  33636  lindsunlem  33637  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  assalactf1o  33648  ply1annprmidl  33700  minplyirredlem  33703  irngnminplynz  33705  algextdeglem4  33711  constrconj  33735  1smat1  33750  madjusmdetlem2  33774  qtophaus  33782  locfinref  33787  zarclssn  33819  zar0ring  33824  zarmxt1  33826  rhmpreimacnlem  33830  rhmpreimacn  33831  metideq  33839  sqsscirc2  33855  tpr2rico  33858  fmcncfil  33877  lmxrge0  33898  lmdvg  33899  qqhval2lem  33927  qqhf  33932  qqhnm  33936  esumle  34022  gsumesum  34023  esumlef  34026  esumrnmpt2  34032  esumpcvgval  34042  esum2d  34057  ofcf  34067  ldsysgenld  34124  ldgenpisyslem1  34127  unelros  34135  difelros  34136  inelsros  34142  diffiunisros  34143  imambfm  34227  omssubadd  34265  inelcarsg  34276  carsgsigalem  34280  carsggect  34283  carsgclctunlem2  34284  oddpwdc  34319  eulerpartlems  34325  eulerpartlemb  34333  eulerpartlemt  34336  iwrdsplit  34352  sseqf  34357  sseqfres  34358  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfrcn0  34494  sgnsub  34509  plymulx0  34524  signsplypnf  34527  signsvtn0  34547  signstfvneq0  34549  signsvtp  34560  signsvtn  34561  fsum2dsub  34584  reprlt  34596  hashreprin  34597  reprgt  34598  reprpmtf1o  34603  chtvalz  34606  breprexplema  34607  breprexplemc  34609  breprexp  34610  circlemeth  34617  logdivsqrle  34627  hgt750lemb  34633  lpadlem3  34655  lpadleft  34660  bnj1536  34830  bnj1001  34935  bnj1280  34996  satffunlem1  35375  satffunlem2  35376  elmrsubrn  35488  neibastop3  36328  finxpsuclem  37363  poimirlem16  37596  poimirlem19  37599  poimirlem20  37600  poimirlem29  37609  mblfinlem3  37619  itg2addnclem3  37633  ftc1cnnclem  37651  lautlt  40048  lautcvr  40049  lauteq  40052  lautco  40054  ltrncl  40082  ltrncnvleN  40087  trljat2  40124  cdlemc6  40153  cdleme20c  40268  cdleme20j  40275  cdleme22e  40301  cdleme22eALTN  40302  cdlemg7aN  40582  cdlemg12e  40604  cdlemg17dALTN  40621  cdlemh  40774  cdlemkfid1N  40878  dibglbN  41123  diblss  41127  diclspsn  41151  dih1  41243  dihglbcpreN  41257  dihmeetlem4preN  41263  lcfrlem19  41518  aks4d1p8d1  42041  evlsvvval  42518  fsuppind  42545  mapfzcons  42672  mzpcl34  42687  mzpindd  42702  mzpsubst  42704  diophrw  42715  diophren  42769  irrapxlem1  42778  pellexlem5  42789  acongrep  42937  pwssplit4  43046  omlimcl2  43203  onexoegt  43205  oasubex  43248  omlim2  43261  nnoeomeqom  43274  nnawordexg  43289  succlg  43290  oacl2g  43292  onmcl  43293  omabs2  43294  omcl2  43295  tfsconcatrev  43310  ofoafg  43316  ofoaf  43317  ofoaass  43322  naddcnfass  43331  naddwordnexlem4  43363  omssrncard  43502  brtrclfv2  43689  rfovcnvf1od  43966  ntrk0kbimka  44001  isotone1  44010  isotone2  44011  4an4132  44470  mulltgt0  44922  fnchoice  44929  3adantlr3  44940  3adantll2  44941  3adantll3  44942  uzwo4  44955  disjf1o  45098  supxrgelem  45252  infleinflem2  45286  xrralrecnnle  45298  supxrunb3  45314  unb2ltle  45330  infrpgernmpt  45380  iooiinicc  45460  iooiinioc  45474  fmuldfeq  45504  mccl  45519  limccog  45541  limcrecl  45550  lptioo1  45553  islpcn  45560  limsupre  45562  neglimc  45568  0ellimcdiv  45570  limclner  45572  climleltrp  45597  climinf3  45637  liminflimsupclim  45728  xlimpnfxnegmnf  45735  icccncfext  45808  fprodcncf  45821  dvnmptdivc  45859  dvnmul  45864  dvmptfprod  45866  dvnprodlem3  45869  stoweidlem25  45946  stoweidlem34  45955  stoweidlem38  45959  stoweidlem44  45965  stoweidlem48  45969  stoweidlem49  45970  stoweidlem59  45980  stoweidlem60  45981  wallispilem4  45989  stirlinglem5  45999  dirkercncflem2  46025  fourierdlem39  46067  fourierdlem42  46070  fourierdlem46  46073  fourierdlem47  46074  fourierdlem48  46075  fourierdlem50  46077  fourierdlem51  46078  fourierdlem64  46091  fourierdlem73  46100  fourierdlem74  46101  fourierdlem77  46104  fourierdlem80  46107  fourierdlem87  46114  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  etransclem32  46187  rrxsnicc  46221  sge0cl  46302  sge0f1o  46303  nnfoctbdjlem  46376  ismeannd  46388  omeiunltfirp  46440  hoicvr  46469  ovncvrrp  46485  hoidmvlelem2  46517  hoidmvlelem5  46520  hspdifhsp  46537  hoiqssbllem2  46544  hspmbllem2  46548  vonicclem2  46605  smflimsuplem7  46747  fundcmpsurbijinj  47284  sqrtpwpw2p  47412  lincresunit2  48207  nnpw2pmod  48317  dignn0flhalflem1  48349  dignn0flhalf  48352  rrx2linest  48476  itsclc0yqsol  48498  itsclc0b  48506  functhinclem1  48708  functhinclem2  48709  fullthinc2  48714