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 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  837  rspc2dv  3618  wereu2  5663  frpomin  6331  funtpg  6593  funcnvtp  6601  funcnvqp  6602  fnund  6654  fun2d  6745  fvun1  6972  iinpreima  7060  ftpg  7146  fsnunf  7175  f1prex  7274  soisores  7316  isotr  7325  off  7681  caofrss  7699  caonncan  7704  fvmpocurryd  8251  oaf1o  8558  omeulem1  8577  oeordi  8582  oelimcl  8595  oeeulem  8596  oeeui  8597  oaabs2  8643  omabs  8645  coflton  8665  pmresg  8859  ralxpmap  8885  domunsncan  9067  sucdom2OLD  9077  sucdom2  9201  unxpdom2  9249  sucxpdom  9250  unblem4  9293  fodomfi  9320  hartogslem1  9532  cantnflt  9662  cantnflem3  9681  cantnflem4  9682  cnfcomlem  9689  cnfcom  9690  ttrcltr  9706  infxpenlem  10003  infxpenc  10008  fseqenlem1  10014  pwsdompw  10194  cfeq0  10246  cofsmo  10259  cfsmolem  10260  ssfin4  10300  hsmexlem4  10419  hsmexlem5  10420  axdc3lem2  10441  fpwwe2  10633  wunpr  10699  mulclpi  10883  mulcanenq  10950  distrlem4pr  11016  prlem934  11023  prlem936  11037  divge0d  13052  elfznelfzob  13734  seqcaopr2  14000  facavg  14257  swrdwrdsymb  14608  cats1un  14667  f1oun2prg  14864  sqrtdiv  15208  sqrtdivd  15366  mulcn2  15536  o1of2  15553  fsumsplit  15683  sumsplit  15710  isumless  15787  demoivreALT  16140  rpnnen2lem11  16163  gcdnncl  16444  qredeu  16591  rpdvds  16593  isprm5  16640  rpexp  16655  divnumden  16680  divdenle  16681  phimullem  16708  phisum  16719  pythagtriplem4  16748  pythagtriplem8  16752  pythagtriplem9  16753  pcgcd1  16806  sumhash  16825  fldivp1  16826  pockthlem  16834  setsfun  17100  setsfun0  17101  ssc2  17765  estrreslem1  18087  estrreslem1OLD  18088  tleile  18373  sgrppropd  18651  mndpropd  18679  grpidssd  18931  grpinvssd  18932  issubg2  19053  isnsg3  19072  eqgid  19092  kerf1ghm  19157  gass  19202  symgextres  19330  gsmsymgreqlem2  19336  sylow1lem5  19507  sylow2alem2  19523  sylow3lem3  19534  efgredlemd  19649  efgredlem  19652  frgpnabllem1  19778  frgpnabllem2  19779  subgdmdprd  19941  ablfacrplem  19972  rglcom4d  20101  issrngd  20689  lmodprop2d  20755  lsspropd  20850  pwssplit1  20892  lspvadd  20929  znidomb  21417  znrrg  21421  lindfind  21671  lindsind  21672  mplsubglem  21859  mplind  21932  mat1ghm  22295  mdetunilem1  22424  mdetunilem3  22426  mdetunilem4  22427  mdetunilem9  22432  cramerimplem2  22496  mat2pmatlin  22547  monmatcollpw  22591  cpmadugsumlemF  22688  mretopd  22906  neiptopnei  22946  neitr  22994  ufilen  23744  flimrest  23797  flimclslem  23798  fclsrest  23838  cnextcn  23881  haustsms2  23951  tsmsxplem2  23968  trust  24044  utoptop  24049  restutop  24052  ustuqtop4  24059  utopsnneiplem  24062  utop2nei  24065  utop3cls  24066  isucn2  24094  ucncn  24100  fmucnd  24107  trcfilu  24109  comet  24332  metustexhalf  24375  metustbl  24385  psmetutop  24386  nrmmetd  24393  reconnlem1  24652  reconnlem2  24653  fsumcn  24698  cmetcaulem  25126  iscmet3lem1  25129  iscmet3lem2  25130  bcthlem5  25166  cmslsschl  25215  rrxdstprj1  25247  minveclem4  25270  ovolfiniun  25340  itg1addlem4  25538  itg1addlem4OLD  25539  itg1addlem5  25540  itgsplitioo  25677  c1liplem1  25839  dvfsumlem1  25870  plyeq0lem  26052  quotcan  26151  psercnlem1  26267  cxplea  26534  birthdaylem3  26789  musumsum  27028  mpodvdsmulf1o  27030  dvdsmulf1o  27032  dchrelbas4  27080  dchrhash  27108  gausslemma2dlem0d  27196  gausslemma2dlem1a  27202  2lgslem1a1  27226  2sqlem8a  27262  2sqlem8  27263  2sqcoprm  27272  2sqmod  27273  chto1ub  27313  vmadivsum  27319  dchrisumlem1  27326  dchrvmasumlem2  27335  dchrvmasumiflem1  27338  rpvmasum2  27349  mulog2sumlem2  27372  selberg2lem  27387  pntrmax  27401  pntpbnd1  27423  pntlemb  27434  pntlemj  27440  noextend  27503  cuteq0  27669  tgjustc1  28150  tgjustc2  28151  ercgrg  28192  motcgr  28211  tglineeltr  28306  colline  28324  miriso  28345  midexlem  28367  perpneq  28389  foot  28397  f1otrg  28546  axcontlem9  28654  uspgr1ewop  28929  nbupgrres  29045  structtocusgr  29127  wlkp1  29362  clwlkl1loop  29464  uspgrn2crct  29486  crctcshwlkn0lem5  29492  3trlond  29850  3pthond  29852  3spthond  29854  frgr3v  29952  vdgn1frgrv2  29973  numclwwlk3  30062  nmblolbii  30476  minvecolem3  30553  minvecolem4  30557  htthlem  30594  bcs2  30859  nmopub2tALT  31586  nmfnleub2  31603  eighmorth  31641  nmophmi  31708  nmopcoadji  31778  hstle  31907  atcvat3i  32073  opreu2reuALT  32141  iinabrex  32224  disjxpin  32243  fmptco1f1o  32281  off2  32290  xppreima2  32300  fgreu  32321  suppovss  32330  1stpreimas  32351  padct  32368  resf1o  32379  fpwrelmap  32382  xrofsup  32404  eliccelico  32412  elicoelioo  32413  iocinif  32416  difioo  32417  suppssnn0  32441  prmdvdsbc  32446  ccatf1  32539  pfxlsw2ccat  32540  wrdt2ind  32541  ressprs  32557  xrge0addgt0  32616  xrge0adddir  32617  gsumhashmul  32635  omndmul3  32658  gsumle  32669  symgcom  32671  pmtrcnel  32677  pmtrcnel2  32678  pmtrcnelor  32679  cycpmfv2  32700  trsp2cyc  32709  cycpmco2lem7  32718  cyc3genpm  32738  cycpmconjslem2  32741  cyc3conja  32743  archirng  32761  archirngz  32762  orngmul  32848  linds2eq  32928  nsgqusf1olem3  32957  ghmquskerlem1  32959  ghmqusker  32963  rhmpreimaidl  32968  lidlunitel  32972  unitpidl1  32973  elrspunidl  32977  drngidl  32982  isprmidlc  32997  qsidomlem1  33002  qsidomlem2  33003  qsnzr  33005  mxidlirredi  33018  mxidlirred  33019  qsdrngi  33040  qsdrnglem2  33041  ressply1evl  33078  deg1le0eq0  33086  ply1degltdimlem  33152  ply1degltdim  33153  lindsunlem  33154  lbsdiflsp0  33156  fedgmullem1  33159  fedgmullem2  33160  ply1annprmidl  33214  minplyirredlem  33215  irngnminplynz  33217  algextdeglem4  33222  1smat1  33239  madjusmdetlem2  33263  qtophaus  33271  locfinref  33276  zarclssn  33308  zar0ring  33313  zarmxt1  33315  rhmpreimacnlem  33319  rhmpreimacn  33320  metideq  33328  sqsscirc2  33344  tpr2rico  33347  fmcncfil  33366  lmxrge0  33387  lmdvg  33388  qqhval2lem  33416  qqhf  33421  qqhnm  33425  esumle  33511  gsumesum  33512  esumlef  33515  esumrnmpt2  33521  esumpcvgval  33531  esum2d  33546  ofcf  33556  ldsysgenld  33613  ldgenpisyslem1  33616  unelros  33624  difelros  33625  inelsros  33631  diffiunisros  33632  imambfm  33716  omssubadd  33754  inelcarsg  33765  carsgsigalem  33769  carsggect  33772  carsgclctunlem2  33773  oddpwdc  33808  eulerpartlems  33814  eulerpartlemb  33822  eulerpartlemt  33825  iwrdsplit  33841  sseqf  33846  sseqfres  33847  ballotlemfc0  33946  ballotlemfcc  33947  ballotlemfrcn0  33983  sgnsub  33998  plymulx0  34013  signsplypnf  34016  signsvtn0  34036  signstfvneq0  34038  signsvtp  34049  signsvtn  34050  fsum2dsub  34074  reprlt  34086  hashreprin  34087  reprgt  34088  reprpmtf1o  34093  chtvalz  34096  breprexplema  34097  breprexplemc  34099  breprexp  34100  circlemeth  34107  logdivsqrle  34117  hgt750lemb  34123  lpadlem3  34145  lpadleft  34150  bnj1536  34320  bnj1001  34425  bnj1280  34486  satffunlem1  34853  satffunlem2  34854  elmrsubrn  34966  neibastop3  35703  finxpsuclem  36734  poimirlem16  36960  poimirlem19  36963  poimirlem20  36964  poimirlem29  36973  mblfinlem3  36983  itg2addnclem3  36997  ftc1cnnclem  37015  lautlt  39418  lautcvr  39419  lauteq  39422  lautco  39424  ltrncl  39452  ltrncnvleN  39457  trljat2  39494  cdlemc6  39523  cdleme20c  39638  cdleme20j  39645  cdleme22e  39671  cdleme22eALTN  39672  cdlemg7aN  39952  cdlemg12e  39974  cdlemg17dALTN  39991  cdlemh  40144  cdlemkfid1N  40248  dibglbN  40493  diblss  40497  diclspsn  40521  dih1  40613  dihglbcpreN  40627  dihmeetlem4preN  40633  lcfrlem19  40888  aks4d1p8d1  41408  evlsvvval  41590  fsuppind  41617  mapfzcons  41909  mzpcl34  41924  mzpindd  41939  mzpsubst  41941  diophrw  41952  diophren  42006  irrapxlem1  42015  pellexlem5  42026  acongrep  42174  pwssplit4  42286  omlimcl2  42446  onexoegt  42448  oasubex  42491  omlim2  42504  nnoeomeqom  42517  nnawordexg  42532  succlg  42533  oacl2g  42535  onmcl  42536  omabs2  42537  omcl2  42538  tfsconcatrev  42553  ofoafg  42559  ofoaf  42560  ofoaass  42565  naddcnfass  42574  naddwordnexlem4  42607  omssrncard  42746  brtrclfv2  42933  rfovcnvf1od  43210  ntrk0kbimka  43245  isotone1  43254  isotone2  43255  4an4132  43715  mulltgt0  44161  fnchoice  44168  3adantlr3  44179  3adantll2  44180  3adantll3  44181  uzwo4  44194  disjf1o  44341  supxrgelem  44498  infleinflem2  44532  xrralrecnnle  44544  supxrunb3  44560  unb2ltle  44576  infrpgernmpt  44626  iooiinicc  44706  iooiinioc  44720  fmuldfeq  44750  mccl  44765  limccog  44787  limcrecl  44796  lptioo1  44799  islpcn  44806  limsupre  44808  neglimc  44814  0ellimcdiv  44816  limclner  44818  climleltrp  44843  climinf3  44883  liminflimsupclim  44974  xlimpnfxnegmnf  44981  icccncfext  45054  fprodcncf  45067  dvnmptdivc  45105  dvnmul  45110  dvmptfprod  45112  dvnprodlem3  45115  stoweidlem25  45192  stoweidlem34  45201  stoweidlem38  45205  stoweidlem44  45211  stoweidlem48  45215  stoweidlem49  45216  stoweidlem59  45226  stoweidlem60  45227  wallispilem4  45235  stirlinglem5  45245  dirkercncflem2  45271  fourierdlem39  45313  fourierdlem42  45316  fourierdlem46  45319  fourierdlem47  45320  fourierdlem48  45321  fourierdlem50  45323  fourierdlem51  45324  fourierdlem64  45337  fourierdlem73  45346  fourierdlem74  45347  fourierdlem77  45350  fourierdlem80  45353  fourierdlem87  45360  fourierdlem94  45367  fourierdlem103  45376  fourierdlem104  45377  etransclem32  45433  rrxsnicc  45467  sge0cl  45548  sge0f1o  45549  nnfoctbdjlem  45622  ismeannd  45634  omeiunltfirp  45686  hoicvr  45715  ovncvrrp  45731  hoidmvlelem2  45763  hoidmvlelem5  45766  hspdifhsp  45783  hoiqssbllem2  45790  hspmbllem2  45794  vonicclem2  45851  smflimsuplem7  45993  fundcmpsurbijinj  46529  sqrtpwpw2p  46657  isomgrref  46954  lincresunit2  47313  nnpw2pmod  47423  dignn0flhalflem1  47455  dignn0flhalf  47458  rrx2linest  47582  itsclc0yqsol  47604  itsclc0b  47612  functhinclem1  47815  functhinclem2  47816  fullthinc2  47821