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  3590  wereu2  5647  frpomin  6343  funtpg  6595  funcnvtp  6603  funcnvqp  6604  fnund  6654  fun2d  6746  fvun1  6976  iinpreima  7069  ftpg  7160  fsnunf  7190  f1prex  7292  soisores  7335  isotr  7344  off  7711  coof  7717  caofrss  7732  caonncan  7737  fvmpocurryd  8288  oaf1o  8571  omeulem1  8590  oeordi  8596  oelimcl  8609  oeeulem  8610  oeeui  8611  oaabs2  8658  omabs  8660  coflton  8680  pmresg  8898  ralxpmap  8924  domunsncan  9096  sucdom2  9218  unxpdom2  9251  sucxpdom  9252  unblem4  9287  fodomfi  9304  hartogslem1  9536  cantnflt  9673  cantnflem3  9692  cantnflem4  9693  cnfcomlem  9700  cnfcom  9701  ttrcltr  9717  infxpenlem  10092  infxpenc  10097  fseqenlem1  10103  pwsdompw  10281  cfeq0  10334  cofsmo  10347  cfsmolem  10348  ssfin4  10388  hsmexlem4  10507  hsmexlem5  10508  axdc3lem2  10529  fpwwe2  10728  wunpr  10794  mulclpi  10978  mulcanenq  11045  distrlem4pr  11111  prlem934  11118  prlem936  11132  divge0d  13204  elfzodif0  13905  elfznelfzob  13909  seqcaopr2  14181  facavg  14445  hashpss  14554  ccatf1  14736  swrdwrdsymb  14812  cats1un  14870  f1oun2prg  15068  sgnsub  15259  sqrtdiv  15432  sqrtdivd  15591  mulcn2  15763  o1of2  15780  fsumsplit  15907  sumsplit  15934  isumless  16014  demoivreALT  16369  rpnnen2lem11  16392  gcdnncl  16677  qredeu  16833  rpdvds  16835  isprm5  16883  rpexp  16898  prmdvdsbc  16902  divnumden  16924  divdenle  16925  phimullem  16956  phisum  16968  pythagtriplem4  16997  pythagtriplem8  17001  pythagtriplem9  17002  pcgcd1  17055  sumhash  17074  fldivp1  17075  pockthlem  17083  setsfun  17349  setsfun0  17350  ssc2  17997  estrreslem1  18311  tleile  18593  chnind  18795  sgrppropd  18920  mndpropd  18951  grpidssd  19226  grpinvssd  19227  issubg2  19352  isnsg3  19370  eqgid  19392  kerf1ghm  19461  ghmqusnsglem1  19494  ghmquskerlem1  19497  ghmqusker  19501  gass  19515  symgextres  19639  gsmsymgreqlem2  19645  sylow1lem5  19816  sylow2alem2  19832  sylow3lem3  19843  efgredlemd  19958  efgredlem  19961  frgpnabllem1  20087  frgpnabllem2  20088  subgdmdprd  20250  ablfacrplem  20281  omndmul3  20348  gsumle  20359  rglcom4d  20437  issrngd  21112  orngmul  21122  lmodprop2d  21199  lsspropd  21292  pwssplit1  21334  lspvadd  21371  drngidl  21539  rhmpreimaidl  21571  isprmidlc  21628  qsidomlem1  21636  qsidomlem2  21637  qsnzr  21639  znidomb  21867  znrrg  21871  lindfind  22122  lindsind  22123  mplsubglem  22306  mplind  22379  evlsvvval  22402  ressply1evl  22688  mat1ghm  22798  mdetunilem1  22927  mdetunilem3  22929  mdetunilem4  22930  mdetunilem9  22935  cramerimplem2  23002  mat2pmatlin  23053  monmatcollpw  23097  cpmadugsumlemF  23194  mretopd  23410  neiptopnei  23450  neitr  23498  ufilen  24249  flimrest  24302  flimclslem  24303  fclsrest  24343  cnextcn  24386  haustsms2  24456  tsmsxplem2  24473  trust  24548  utoptop  24553  restutop  24556  ustuqtop4  24563  utopsnneiplem  24566  utop2nei  24569  utop3cls  24570  isucn2  24597  ucncn  24603  fmucnd  24610  trcfilu  24612  comet  24832  metustexhalf  24875  metustbl  24885  psmetutop  24886  nrmmetd  24893  reconnlem1  25146  reconnlem2  25147  fsumcn  25191  cmetcaulem  25609  iscmet3lem1  25612  iscmet3lem2  25613  bcthlem5  25649  cmslsschl  25698  rrxdstprj1  25730  minveclem4  25753  ovolfiniun  25822  itg1addlem4  26020  itg1addlem5  26021  itgsplitioo  26158  c1liplem1  26316  dvfsumlem1  26346  plyeq0lem  26529  plyn0mulidp  26602  quotcan  26632  psercnlem1  26752  cxplea  27024  birthdaylem3  27281  musumsum  27519  mpodvdsmulf1o  27521  dvdsmulf1o  27523  dchrelbas4  27570  dchrhash  27598  gausslemma2dlem0d  27686  gausslemma2dlem1a  27692  2lgslem1a1  27716  2sqlem8a  27752  2sqlem8  27753  2sqcoprm  27762  2sqmod  27763  chto1ub  27803  vmadivsum  27809  dchrisumlem1  27816  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  rpvmasum2  27839  mulog2sumlem2  27862  selberg2lem  27877  pntrmax  27891  pntpbnd1  27913  pntlemb  27924  pntlemj  27930  noextend  28023  cuteq0  28201  tgjustc1  28937  tgjustc2  28938  ercgrg  28980  motcgr  28999  tglineeltr  29099  colline  29118  miriso  29142  midexlem  29164  perpneq  29189  foot  29197  f1otrg  29448  axcontlem9  29550  uspgr1ewop  29829  nbupgrres  29945  structtocusgr  30027  wlkp1  30260  clwlkl1loop  30370  uspgrn2crct  30397  crctcshwlkn0lem5  30403  3trlond  30774  3pthond  30776  3spthond  30778  frgr3v  30876  vdgn1frgrv2  30897  numclwwlk3  30986  nmblolbii  31401  minvecolem3  31478  minvecolem4  31482  htthlem  31519  bcs2  31784  nmopub2tALT  32511  nmfnleub2  32528  eighmorth  32566  nmophmi  32633  nmopcoadji  32703  hstle  32832  atcvat3i  32998  opreu2reuALT  33073  prssad  33125  prssbd  33126  iinabrex  33163  disjxpin  33182  fmptco1f1o  33227  off2  33235  xppreima2  33245  fgreu  33265  suppovss  33274  1stpreimas  33299  padct  33310  resf1o  33322  fpwrelmap  33325  arginv  33339  argcj  33340  xrofsup  33359  eliccelico  33369  elicoelioo  33370  iocinif  33373  difioo  33374  suppssnn0  33397  elq2  33403  2exple2exp  33425  oexpled  33427  indsupp  33434  indfsid  33436  pfxlsw2ccat  33513  wrdt2ind  33516  ressprs  33527  xrge0addgt0  33578  xrge0adddir  33579  mndlactf1o  33591  mndractf1o  33592  gsumhashmul  33628  gsummulsubdishift1  33629  symgcom  33644  pmtrcnel  33650  pmtrcnel2  33651  pmtrcnelor  33652  cycpmfv2  33675  trsp2cyc  33684  cycpmco2lem7  33693  cyc3genpm  33713  cycpmconjslem2  33716  cyc3conja  33718  archirng  33749  archirngz  33750  rlocf1  33835  rlocisunit  33837  rrgsubm  33845  fracerl  33868  idomsubr  33871  linds2eq  33936  nsgqusf1olem3  33966  lidlunitel  33973  unitpidl1  33974  elrspunidl  33978  mxidlirredi  33996  mxidlirred  33997  qsdrngi  34019  qsdrnglem2  34020  dflring2  34025  rprmasso  34057  1arithidomlem2  34068  1arithufdlem4  34079  zringidom  34083  deg1le0eq0  34105  ply1unit  34107  ply1dg1rt  34112  ply1dg3rt0irred  34116  m1pmeq  34117  selvply1rhmlema  34150  selvply1rhmlem1  34152  evlextv  34174  mplvrpmrhm  34179  esplympl  34199  esplysply  34203  esplyind  34207  esplyindfv  34208  vietadeg1  34210  ply1degltdimlem  34254  ply1degltdim  34255  lindsunlem  34256  lbsdiflsp0  34258  fedgmullem1  34261  fedgmullem2  34262  assalactf1o  34267  ply1annprmidl  34339  minplyirredlem  34342  irngnminplynz  34344  minplyelirng  34347  algextdeglem4  34352  constrconj  34377  constrsqrtcl  34411  cos9thpiminplylem1  34414  cos9thpiminplylem2  34415  cos9thpinconstrlem1  34421  1smat1  34436  madjusmdetlem2  34460  qtophaus  34468  locfinref  34473  zarclssn  34505  zar0ring  34510  zarmxt1  34512  rhmpreimacnlem  34516  rhmpreimacn  34517  metideq  34525  sqsscirc2  34541  tpr2rico  34544  fmcncfil  34563  lmxrge0  34584  lmdvg  34585  qqhval2lem  34613  qqhf  34618  qqhnm  34622  esumle  34690  gsumesum  34691  esumlef  34694  esumrnmpt2  34700  esumpcvgval  34710  esum2d  34725  ofcf  34735  ldsysgenld  34793  ldgenpisyslem1  34796  unelros  34804  difelros  34805  inelsros  34811  diffiunisros  34812  imambfm  34894  omssubadd  34932  inelcarsg  34943  carsgsigalem  34947  carsggect  34950  carsgclctunlem2  34951  oddpwdc  34986  eulerpartlems  34992  eulerpartlemb  35000  eulerpartlemt  35003  iwrdsplit  35019  sseqf  35024  sseqfres  35025  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemfrcn0  35162  signsplypnf  35179  signsvtn0  35199  signstfvneq0  35201  signsvtp  35212  signsvtn  35213  fsum2dsub  35236  reprlt  35248  hashreprin  35249  reprgt  35250  reprpmtf1o  35255  chtvalz  35258  breprexplema  35259  breprexplemc  35261  breprexp  35262  circlemeth  35269  logdivsqrle  35279  hgt750lemb  35285  lpadlem3  35310  lpadleft  35315  bnj1536  35484  bnj1001  35589  bnj1280  35650  fineqvnttrclselem2  35790  satffunlem1  36172  satffunlem2  36173  elmrsubrn  36285  neibastop3  37150  finxpsuclem  38321  poimirlem16  38555  poimirlem19  38558  poimirlem20  38559  poimirlem29  38568  mblfinlem3  38578  itg2addnclem3  38592  ftc1cnnclem  38610  lautlt  41149  lautcvr  41150  lauteq  41153  lautco  41155  ltrncl  41183  ltrncnvleN  41188  trljat2  41225  cdlemc6  41254  cdleme20c  41369  cdleme20j  41376  cdleme22e  41402  cdleme22eALTN  41403  cdlemg7aN  41683  cdlemg12e  41705  cdlemg17dALTN  41722  cdlemh  41875  cdlemkfid1N  41979  dibglbN  42224  diblss  42228  diclspsn  42252  dih1  42344  dihglbcpreN  42358  dihmeetlem4preN  42364  lcfrlem19  42619  aks4d1p8d1  43135  fsuppind  43619  mapfzcons  43727  mzpcl34  43742  mzpindd  43757  mzpsubst  43759  diophrw  43770  diophren  43820  irrapxlem1  43829  pellexlem5  43840  acongrep  43987  pwssplit4  44091  omlimcl2  44244  onexoegt  44246  oasubex  44288  omlim2  44301  nnoeomeqom  44314  nnawordexg  44329  succlg  44330  oacl2g  44332  onmcl  44333  omabs2  44334  omcl2  44335  tfsconcatrev  44350  ofoafg  44356  ofoaf  44357  ofoaass  44362  naddcnfass  44371  naddwordnexlem4  44403  omssrncard  44541  brtrclfv2  44727  rfovcnvf1od  45004  ntrk0kbimka  45039  isotone1  45048  isotone2  45049  4an4132  45482  modelaxrep  45971  mulltgt0  46039  fnchoice  46046  3adantlr3  46057  3adantll2  46058  3adantll3  46059  uzwo4  46070  disjf1o  46206  supxrgelem  46349  infleinflem2  46382  xrralrecnnle  46394  supxrunb3  46410  unb2ltle  46425  infrpgernmpt  46475  iooiinicc  46554  iooiinioc  46568  fmuldfeq  46595  mccl  46610  limccog  46632  limcrecl  46641  lptioo1  46644  islpcn  46649  limsupre  46651  neglimc  46657  0ellimcdiv  46659  limclner  46661  climleltrp  46686  climinf3  46726  liminflimsupclim  46817  xlimpnfxnegmnf  46824  icccncfext  46897  fprodcncf  46910  dvnmptdivc  46948  dvnmul  46953  dvmptfprod  46955  dvnprodlem3  46958  stoweidlem25  47035  stoweidlem34  47044  stoweidlem38  47048  stoweidlem44  47054  stoweidlem48  47058  stoweidlem49  47059  stoweidlem59  47069  stoweidlem60  47070  wallispilem4  47078  stirlinglem5  47088  dirkercncflem2  47114  fourierdlem39  47156  fourierdlem42  47159  fourierdlem46  47162  fourierdlem47  47163  fourierdlem48  47164  fourierdlem50  47166  fourierdlem51  47167  fourierdlem64  47180  fourierdlem73  47189  fourierdlem74  47190  fourierdlem77  47193  fourierdlem80  47196  fourierdlem87  47203  fourierdlem94  47210  fourierdlem103  47219  fourierdlem104  47220  etransclem32  47276  rrxsnicc  47310  sge0cl  47391  sge0f1o  47392  nnfoctbdjlem  47465  ismeannd  47477  omeiunltfirp  47529  ovncvrrp  47574  hoidmvlelem2  47606  hoidmvlelem5  47609  hspdifhsp  47626  hoiqssbllem2  47633  hspmbllem2  47637  vonicclem2  47694  smflimsuplem7  47836  tmachlem-agreeprod  47947  fundcmpsurbijinj  48492  sqrtpwpw2p  48623  lincresunit2  49590  nnpw2pmod  49695  dignn0flhalflem1  49727  dignn0flhalf  49730  rrx2linest  49854  itsclc0yqsol  49876  itsclc0b  49884  brab2dd  49938  oppcendc  50126  imaidfu  50218  imasubc  50259  oppcthinendcALT  50549  functhinclem1  50552  functhinclem2  50553  fullthinc2  50559