Theorem syl21anc 851

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bibiad  853  syl1111anc  854  rspc2dv  3594  wereu2  5652  frpomin  6358  funtpg  6614  funcnvtp  6622  funcnvqp  6623  fnund  6673  fun2d  6765  fvun1  6996  iinpreima  7090  ftpg  7181  fsnunf  7210  f1prex  7312  soisores  7355  isotr  7364  off  7732  coof  7738  caofrss  7753  caonncan  7758  fvmpocurryd  8313  oaf1o  8596  omeulem1  8615  oeordi  8621  oelimcl  8634  oeeulem  8635  oeeui  8636  oaabs2  8683  omabs  8685  coflton  8705  pmresg  8923  ralxpmap  8949  domunsncan  9121  sucdom2  9243  unxpdom2  9276  sucxpdom  9277  unblem4  9312  fodomfi  9329  hartogslem1  9560  cantnflt  9697  cantnflem3  9716  cantnflem4  9717  cnfcomlem  9724  cnfcom  9725  ttrcltr  9741  infxpenlem  10116  infxpenc  10121  fseqenlem1  10127  pwsdompw  10305  cfeq0  10358  cofsmo  10371  cfsmolem  10372  ssfin4  10412  hsmexlem4  10531  hsmexlem5  10532  axdc3lem2  10553  fpwwe2  10752  wunpr  10818  mulclpi  11002  mulcanenq  11069  distrlem4pr  11135  prlem934  11142  prlem936  11156  divge0d  13228  elfzodif0  13929  elfznelfzob  13933  seqcaopr2  14205  facavg  14469  hashpss  14578  ccatf1  14760  swrdwrdsymb  14837  cats1un  14895  f1oun2prg  15094  sgnsub  15285  sqrtdiv  15458  sqrtdivd  15617  mulcn2  15789  o1of2  15806  fsumsplit  15933  sumsplit  15960  isumless  16040  demoivreALT  16395  rpnnen2lem11  16418  gcdnncl  16703  qredeu  16859  rpdvds  16861  isprm5  16909  rpexp  16924  prmdvdsbc  16928  divnumden  16950  divdenle  16951  phimullem  16982  phisum  16994  pythagtriplem4  17023  pythagtriplem8  17027  pythagtriplem9  17028  pcgcd1  17081  sumhash  17100  fldivp1  17101  pockthlem  17109  setsfun  17375  setsfun0  17376  ssc2  18023  estrreslem1  18337  tleile  18619  chnind  18821  sgrppropd  18946  mndpropd  18977  grpidssd  19252  grpinvssd  19253  issubg2  19378  isnsg3  19396  eqgid  19418  kerf1ghm  19487  ghmqusnsglem1  19521  ghmquskerlem1  19524  ghmqusker  19528  gass  19542  symgextres  19666  gsmsymgreqlem2  19672  sylow1lem5  19843  sylow2alem2  19859  sylow3lem3  19870  efgredlemd  19985  efgredlem  19988  frgpnabllem1  20114  frgpnabllem2  20115  subgdmdprd  20277  ablfacrplem  20308  omndmul3  20375  gsumle  20386  rglcom4d  20464  issrngd  21139  orngmul  21149  lmodprop2d  21226  lsspropd  21319  pwssplit1  21361  lspvadd  21398  drngidl  21566  rhmpreimaidl  21598  isprmidlc  21655  qsidomlem1  21663  qsidomlem2  21664  qsnzr  21666  znidomb  21894  znrrg  21898  lindfind  22149  lindsind  22150  mplsubglem  22333  mplind  22406  evlsvvval  22429  ressply1evl  22715  mat1ghm  22825  mdetunilem1  22954  mdetunilem3  22956  mdetunilem4  22957  mdetunilem9  22962  cramerimplem2  23029  mat2pmatlin  23080  monmatcollpw  23124  cpmadugsumlemF  23221  mretopd  23437  neiptopnei  23477  neitr  23525  ufilen  24276  flimrest  24329  flimclslem  24330  fclsrest  24370  cnextcn  24413  haustsms2  24483  tsmsxplem2  24500  trust  24575  utoptop  24580  restutop  24583  ustuqtop4  24590  utopsnneiplem  24593  utop2nei  24596  utop3cls  24597  isucn2  24624  ucncn  24630  fmucnd  24637  trcfilu  24639  comet  24859  metustexhalf  24902  metustbl  24912  psmetutop  24913  nrmmetd  24920  reconnlem1  25173  reconnlem2  25174  fsumcn  25218  cmetcaulem  25636  iscmet3lem1  25639  iscmet3lem2  25640  bcthlem5  25676  cmslsschl  25725  rrxdstprj1  25757  minveclem4  25780  ovolfiniun  25849  itg1addlem4  26047  itg1addlem5  26048  itgsplitioo  26185  c1liplem1  26343  dvfsumlem1  26373  plyeq0lem  26556  plyn0mulidp  26629  quotcan  26659  psercnlem1  26779  cxplea  27051  birthdaylem3  27308  musumsum  27546  mpodvdsmulf1o  27548  dvdsmulf1o  27550  dchrelbas4  27597  dchrhash  27625  gausslemma2dlem0d  27713  gausslemma2dlem1a  27719  2lgslem1a1  27743  2sqlem8a  27779  2sqlem8  27780  2sqcoprm  27789  2sqmod  27790  chto1ub  27830  vmadivsum  27836  dchrisumlem1  27843  dchrvmasumlem2  27852  dchrvmasumiflem1  27855  rpvmasum2  27866  mulog2sumlem2  27889  selberg2lem  27904  pntrmax  27918  pntpbnd1  27940  pntlemb  27951  pntlemj  27957  noextend  28050  cuteq0  28228  tgjustc1  28964  tgjustc2  28965  ercgrg  29007  motcgr  29026  tglineeltr  29126  colline  29145  miriso  29169  midexlem  29191  perpneq  29216  foot  29224  f1otrg  29475  axcontlem9  29577  uspgr1ewop  29856  nbupgrres  29972  structtocusgr  30054  wlkp1  30287  clwlkl1loop  30397  uspgrn2crct  30424  crctcshwlkn0lem5  30430  3trlond  30801  3pthond  30803  3spthond  30805  frgr3v  30903  vdgn1frgrv2  30924  numclwwlk3  31013  nmblolbii  31428  minvecolem3  31505  minvecolem4  31509  htthlem  31546  bcs2  31811  nmopub2tALT  32538  nmfnleub2  32555  eighmorth  32593  nmophmi  32660  nmopcoadji  32730  hstle  32859  atcvat3i  33025  opreu2reuALT  33142  prssad  33194  prssbd  33195  iinabrex  33232  disjxpin  33251  fmptco1f1o  33296  off2  33304  xppreima2  33314  fgreu  33334  suppovss  33342  1stpreimas  33367  padct  33378  resf1o  33389  fpwrelmap  33392  arginv  33406  argcj  33407  xrofsup  33426  eliccelico  33436  elicoelioo  33437  iocinif  33440  difioo  33441  suppssnn0  33464  elq2  33470  2exple2exp  33492  oexpled  33494  indsupp  33501  indfsid  33503  pfxlsw2ccat  33580  wrdt2ind  33583  ressprs  33594  xrge0addgt0  33645  xrge0adddir  33646  mndlactf1o  33658  mndractf1o  33659  gsumhashmul  33695  gsummulsubdishift1  33696  symgcom  33711  pmtrcnel  33717  pmtrcnel2  33718  pmtrcnelor  33719  cycpmfv2  33742  trsp2cyc  33751  cycpmco2lem7  33760  cyc3genpm  33780  cycpmconjslem2  33783  cyc3conja  33785  archirng  33816  archirngz  33817  rlocf1  33902  rlocisunit  33904  rrgsubm  33912  fracerl  33935  idomsubr  33938  linds2eq  34003  nsgqusf1olem3  34033  lidlunitel  34040  unitpidl1  34041  elrspunidl  34045  mxidlirredi  34063  mxidlirred  34064  qsdrngi  34086  qsdrnglem2  34087  dflring2  34092  rprmasso  34124  1arithidomlem2  34135  1arithufdlem4  34146  zringidom  34150  deg1le0eq0  34172  ply1unit  34174  ply1dg1rt  34179  ply1dg3rt0irred  34183  m1pmeq  34184  selvply1rhmlema  34217  selvply1rhmlem1  34219  evlextv  34241  mplvrpmrhm  34246  esplympl  34266  esplysply  34270  esplyind  34274  esplyindfv  34275  vietadeg1  34277  ply1degltdimlem  34321  ply1degltdim  34322  lindsunlem  34323  lbsdiflsp0  34325  fedgmullem1  34328  fedgmullem2  34329  assalactf1o  34334  ply1annprmidl  34406  minplyirredlem  34409  irngnminplynz  34411  minplyelirng  34414  algextdeglem4  34419  constrconj  34444  constrsqrtcl  34478  cos9thpiminplylem1  34481  cos9thpiminplylem2  34482  cos9thpinconstrlem1  34488  1smat1  34503  madjusmdetlem2  34527  qtophaus  34535  locfinref  34540  zarclssn  34572  zar0ring  34577  zarmxt1  34579  rhmpreimacnlem  34583  rhmpreimacn  34584  metideq  34592  sqsscirc2  34608  tpr2rico  34611  fmcncfil  34630  lmxrge0  34651  lmdvg  34652  qqhval2lem  34680  qqhf  34685  qqhnm  34689  esumle  34757  gsumesum  34758  esumlef  34761  esumrnmpt2  34767  esumpcvgval  34777  esum2d  34792  ofcf  34802  ldsysgenld  34860  ldgenpisyslem1  34863  unelros  34871  difelros  34872  inelsros  34878  diffiunisros  34879  imambfm  34961  omssubadd  34999  inelcarsg  35010  carsgsigalem  35014  carsggect  35017  carsgclctunlem2  35018  oddpwdc  35053  eulerpartlems  35059  eulerpartlemb  35067  eulerpartlemt  35070  iwrdsplit  35086  sseqf  35091  sseqfres  35092  ballotlemfc0  35192  ballotlemfcc  35193  ballotlemfrcn0  35229  signsplypnf  35246  signsvtn0  35266  signstfvneq0  35268  signsvtp  35279  signsvtn  35280  fsum2dsub  35303  reprlt  35315  hashreprin  35316  reprgt  35317  reprpmtf1o  35322  chtvalz  35325  breprexplema  35326  breprexplemc  35328  breprexp  35329  circlemeth  35336  logdivsqrle  35346  hgt750lemb  35352  lpadlem3  35377  lpadleft  35382  bnj1536  35551  bnj1001  35656  bnj1280  35717  fineqvnttrclselem2  35889  satffunlem1  36338  satffunlem2  36339  elmrsubrn  36451  neibastop3  37327  finxpsuclem  38511  poimirlem16  38745  poimirlem19  38748  poimirlem20  38749  poimirlem29  38758  mblfinlem3  38768  itg2addnclem3  38782  ftc1cnnclem  38800  lautlt  41339  lautcvr  41340  lauteq  41343  lautco  41345  ltrncl  41373  ltrncnvleN  41378  trljat2  41415  cdlemc6  41444  cdleme20c  41559  cdleme20j  41566  cdleme22e  41592  cdleme22eALTN  41593  cdlemg7aN  41873  cdlemg12e  41895  cdlemg17dALTN  41912  cdlemh  42065  cdlemkfid1N  42169  dibglbN  42414  diblss  42418  diclspsn  42442  dih1  42534  dihglbcpreN  42548  dihmeetlem4preN  42554  lcfrlem19  42809  aks4d1p8d1  43325  fsuppind  43809  mapfzcons  43918  mzpcl34  43933  mzpindd  43948  mzpsubst  43950  diophrw  43961  diophren  44011  irrapxlem1  44020  pellexlem5  44031  acongrep  44178  pwssplit4  44282  omlimcl2  44434  onexoegt  44436  oasubex  44478  omlim2  44491  nnoeomeqom  44504  nnawordexg  44519  succlg  44520  oacl2g  44522  onmcl  44523  omabs2  44524  omcl2  44525  tfsconcatrev  44540  ofoafg  44546  ofoaf  44547  ofoaass  44552  naddcnfass  44561  naddwordnexlem4  44593  omssrncard  44731  brtrclfv2  44917  rfovcnvf1od  45194  ntrk0kbimka  45229  isotone1  45238  isotone2  45239  4an4132  45671  modelaxrep  46164  mulltgt0  46242  fnchoice  46249  3adantlr3  46260  3adantll2  46261  3adantll3  46262  uzwo4  46273  disjf1o  46409  supxrgelem  46552  infleinflem2  46585  xrralrecnnle  46597  supxrunb3  46613  unb2ltle  46628  infrpgernmpt  46678  iooiinicc  46757  iooiinioc  46771  fmuldfeq  46798  mccl  46813  limccog  46835  limcrecl  46844  lptioo1  46847  islpcn  46852  limsupre  46854  neglimc  46860  0ellimcdiv  46862  limclner  46864  climleltrp  46889  climinf3  46929  liminflimsupclim  47020  xlimpnfxnegmnf  47027  icccncfext  47100  fprodcncf  47113  dvnmptdivc  47151  dvnmul  47156  dvmptfprod  47158  dvnprodlem3  47161  stoweidlem25  47238  stoweidlem34  47247  stoweidlem38  47251  stoweidlem44  47257  stoweidlem48  47261  stoweidlem49  47262  stoweidlem59  47272  stoweidlem60  47273  wallispilem4  47281  stirlinglem5  47291  dirkercncflem2  47317  fourierdlem39  47359  fourierdlem42  47362  fourierdlem46  47365  fourierdlem47  47366  fourierdlem48  47367  fourierdlem50  47369  fourierdlem51  47370  fourierdlem64  47383  fourierdlem73  47392  fourierdlem74  47393  fourierdlem77  47396  fourierdlem80  47399  fourierdlem87  47406  fourierdlem94  47413  fourierdlem103  47422  fourierdlem104  47423  etransclem32  47479  rrxsnicc  47513  sge0cl  47594  sge0f1o  47595  nnfoctbdjlem  47668  ismeannd  47680  omeiunltfirp  47732  ovncvrrp  47777  hoidmvlelem2  47809  hoidmvlelem5  47812  hspdifhsp  47829  hoiqssbllem2  47836  hspmbllem2  47840  vonicclem2  47897  smflimsuplem7  48039  tmachlem-agreeprod  48150  fundcmpsurbijinj  48695  sqrtpwpw2p  48826  lincresunit2  49793  nnpw2pmod  49898  dignn0flhalflem1  49930  dignn0flhalf  49933  rrx2linest  50057  itsclc0yqsol  50079  itsclc0b  50087  brab2dd  50142  oppcendc  50335  imaidfu  50429  imasubc  50470  oppcthinendcALT  50779  functhinclem1  50782  functhinclem2  50783  fullthinc2  50789