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 584	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:  bibiad  839  syl1111anc  840  rspc2dv  3594  wereu2  5620  frpomin  6292  funtpg  6541  funcnvtp  6549  funcnvqp  6550  fnund  6601  fun2d  6692  fvun1  6918  iinpreima  7007  ftpg  7094  fsnunf  7125  f1prex  7225  soisores  7268  isotr  7277  off  7635  coof  7641  caofrss  7656  caonncan  7661  fvmpocurryd  8211  oaf1o  8488  omeulem1  8507  oeordi  8512  oelimcl  8525  oeeulem  8526  oeeui  8527  oaabs2  8574  omabs  8576  coflton  8596  pmresg  8804  ralxpmap  8830  domunsncan  9001  sucdom2  9127  unxpdom2  9159  sucxpdom  9160  unblem4  9200  fodomfi  9219  fodomfiOLD  9239  hartogslem1  9453  cantnflt  9587  cantnflem3  9606  cantnflem4  9607  cnfcomlem  9614  cnfcom  9615  ttrcltr  9631  infxpenlem  9926  infxpenc  9931  fseqenlem1  9937  pwsdompw  10116  cfeq0  10169  cofsmo  10182  cfsmolem  10183  ssfin4  10223  hsmexlem4  10342  hsmexlem5  10343  axdc3lem2  10364  fpwwe2  10556  wunpr  10622  mulclpi  10806  mulcanenq  10873  distrlem4pr  10939  prlem934  10946  prlem936  10960  divge0d  12995  elfznelfzob  13694  seqcaopr2  13963  facavg  14226  swrdwrdsymb  14587  cats1un  14645  f1oun2prg  14842  sqrtdiv  15190  sqrtdivd  15349  mulcn2  15521  o1of2  15538  fsumsplit  15666  sumsplit  15693  isumless  15770  demoivreALT  16128  rpnnen2lem11  16151  gcdnncl  16436  qredeu  16587  rpdvds  16589  isprm5  16636  rpexp  16651  prmdvdsbc  16655  divnumden  16677  divdenle  16678  phimullem  16708  phisum  16720  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  pcgcd1  16807  sumhash  16826  fldivp1  16827  pockthlem  16835  setsfun  17100  setsfun0  17101  ssc2  17747  estrreslem1  18061  tleile  18343  sgrppropd  18623  mndpropd  18651  grpidssd  18913  grpinvssd  18914  issubg2  19038  isnsg3  19057  eqgid  19077  kerf1ghm  19144  ghmqusnsglem1  19177  ghmquskerlem1  19180  ghmqusker  19184  gass  19198  symgextres  19322  gsmsymgreqlem2  19328  sylow1lem5  19499  sylow2alem2  19515  sylow3lem3  19526  efgredlemd  19641  efgredlem  19644  frgpnabllem1  19770  frgpnabllem2  19771  subgdmdprd  19933  ablfacrplem  19964  omndmul3  20031  gsumle  20042  rglcom4d  20114  issrngd  20758  orngmul  20768  lmodprop2d  20845  lsspropd  20939  pwssplit1  20981  lspvadd  21018  rhmpreimaidl  21202  znidomb  21486  znrrg  21490  lindfind  21741  lindsind  21742  mplsubglem  21924  mplind  21993  ressply1evl  22273  mat1ghm  22386  mdetunilem1  22515  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  cramerimplem2  22587  mat2pmatlin  22638  monmatcollpw  22682  cpmadugsumlemF  22779  mretopd  22995  neiptopnei  23035  neitr  23083  ufilen  23833  flimrest  23886  flimclslem  23887  fclsrest  23927  cnextcn  23970  haustsms2  24040  tsmsxplem2  24057  trust  24133  utoptop  24138  restutop  24141  ustuqtop4  24148  utopsnneiplem  24151  utop2nei  24154  utop3cls  24155  isucn2  24182  ucncn  24188  fmucnd  24195  trcfilu  24197  comet  24417  metustexhalf  24460  metustbl  24470  psmetutop  24471  nrmmetd  24478  reconnlem1  24731  reconnlem2  24732  fsumcn  24777  cmetcaulem  25204  iscmet3lem1  25207  iscmet3lem2  25208  bcthlem5  25244  cmslsschl  25293  rrxdstprj1  25325  minveclem4  25348  ovolfiniun  25418  itg1addlem4  25616  itg1addlem5  25617  itgsplitioo  25755  c1liplem1  25917  dvfsumlem1  25948  plyeq0lem  26131  quotcan  26233  psercnlem1  26351  cxplea  26621  birthdaylem3  26879  musumsum  27118  mpodvdsmulf1o  27120  dvdsmulf1o  27122  dchrelbas4  27170  dchrhash  27198  gausslemma2dlem0d  27286  gausslemma2dlem1a  27292  2lgslem1a1  27316  2sqlem8a  27352  2sqlem8  27353  2sqcoprm  27362  2sqmod  27363  chto1ub  27403  vmadivsum  27409  dchrisumlem1  27416  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  rpvmasum2  27439  mulog2sumlem2  27462  selberg2lem  27477  pntrmax  27491  pntpbnd1  27513  pntlemb  27524  pntlemj  27530  noextend  27594  cuteq0  27764  tgjustc1  28438  tgjustc2  28439  ercgrg  28480  motcgr  28499  tglineeltr  28594  colline  28612  miriso  28633  midexlem  28655  perpneq  28677  foot  28685  f1otrg  28834  axcontlem9  28935  uspgr1ewop  29211  nbupgrres  29327  structtocusgr  29409  wlkp1  29643  clwlkl1loop  29746  uspgrn2crct  29771  crctcshwlkn0lem5  29777  3trlond  30135  3pthond  30137  3spthond  30139  frgr3v  30237  vdgn1frgrv2  30258  numclwwlk3  30347  nmblolbii  30761  minvecolem3  30838  minvecolem4  30842  htthlem  30879  bcs2  31144  nmopub2tALT  31871  nmfnleub2  31888  eighmorth  31926  nmophmi  31993  nmopcoadji  32063  hstle  32192  atcvat3i  32358  opreu2reuALT  32439  prssad  32491  prssbd  32492  iinabrex  32531  disjxpin  32550  fmptco1f1o  32590  off2  32598  xppreima2  32608  fgreu  32629  suppovss  32637  1stpreimas  32662  padct  32676  resf1o  32686  fpwrelmap  32689  arginv  32704  argcj  32705  xrofsup  32723  eliccelico  32733  elicoelioo  32734  iocinif  32737  difioo  32738  elfzodif0  32750  suppssnn0  32763  hashpss  32767  elq2  32769  sgnsub  32795  2exple2exp  32803  oexpled  32805  indsupp  32823  ccatf1  32903  pfxlsw2ccat  32905  wrdt2ind  32908  ressprs  32921  chnind  32966  xrge0addgt0  32984  xrge0adddir  32985  mndlactf1o  32997  mndractf1o  32998  gsumhashmul  33027  symgcom  33038  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  cycpmfv2  33069  trsp2cyc  33078  cycpmco2lem7  33087  cyc3genpm  33107  cycpmconjslem2  33110  cyc3conja  33112  archirng  33140  archirngz  33141  rlocf1  33223  rrgsubm  33233  fracerl  33255  idomsubr  33258  linds2eq  33328  nsgqusf1olem3  33362  lidlunitel  33370  unitpidl1  33371  elrspunidl  33375  drngidl  33380  isprmidlc  33394  qsidomlem1  33399  qsidomlem2  33400  qsnzr  33402  mxidlirredi  33418  mxidlirred  33419  qsdrngi  33442  qsdrnglem2  33443  rprmasso  33472  1arithidomlem2  33483  1arithufdlem4  33494  zringidom  33498  deg1le0eq0  33518  ply1unit  33520  ply1dg1rt  33524  ply1dg3rt0irred  33527  m1pmeq  33528  ply1degltdimlem  33594  ply1degltdim  33595  lindsunlem  33596  lbsdiflsp0  33598  fedgmullem1  33601  fedgmullem2  33602  assalactf1o  33607  ply1annprmidl  33673  minplyirredlem  33676  irngnminplynz  33678  minplyelirng  33681  algextdeglem4  33686  constrconj  33711  constrsqrtcl  33745  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  cos9thpinconstrlem1  33755  1smat1  33770  madjusmdetlem2  33794  qtophaus  33802  locfinref  33807  zarclssn  33839  zar0ring  33844  zarmxt1  33846  rhmpreimacnlem  33850  rhmpreimacn  33851  metideq  33859  sqsscirc2  33875  tpr2rico  33878  fmcncfil  33897  lmxrge0  33918  lmdvg  33919  qqhval2lem  33947  qqhf  33952  qqhnm  33956  esumle  34024  gsumesum  34025  esumlef  34028  esumrnmpt2  34034  esumpcvgval  34044  esum2d  34059  ofcf  34069  ldsysgenld  34126  ldgenpisyslem1  34129  unelros  34137  difelros  34138  inelsros  34144  diffiunisros  34145  imambfm  34229  omssubadd  34267  inelcarsg  34278  carsgsigalem  34282  carsggect  34285  carsgclctunlem2  34286  oddpwdc  34321  eulerpartlems  34327  eulerpartlemb  34335  eulerpartlemt  34338  iwrdsplit  34354  sseqf  34359  sseqfres  34360  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemfrcn0  34497  plymulx0  34514  signsplypnf  34517  signsvtn0  34537  signstfvneq0  34539  signsvtp  34550  signsvtn  34551  fsum2dsub  34574  reprlt  34586  hashreprin  34587  reprgt  34588  reprpmtf1o  34593  chtvalz  34596  breprexplema  34597  breprexplemc  34599  breprexp  34600  circlemeth  34607  logdivsqrle  34617  hgt750lemb  34623  lpadlem3  34645  lpadleft  34650  bnj1536  34820  bnj1001  34925  bnj1280  34986  satffunlem1  35379  satffunlem2  35380  elmrsubrn  35492  neibastop3  36335  finxpsuclem  37370  poimirlem16  37615  poimirlem19  37618  poimirlem20  37619  poimirlem29  37628  mblfinlem3  37638  itg2addnclem3  37652  ftc1cnnclem  37670  lautlt  40070  lautcvr  40071  lauteq  40074  lautco  40076  ltrncl  40104  ltrncnvleN  40109  trljat2  40146  cdlemc6  40175  cdleme20c  40290  cdleme20j  40297  cdleme22e  40323  cdleme22eALTN  40324  cdlemg7aN  40604  cdlemg12e  40626  cdlemg17dALTN  40643  cdlemh  40796  cdlemkfid1N  40900  dibglbN  41145  diblss  41149  diclspsn  41173  dih1  41265  dihglbcpreN  41279  dihmeetlem4preN  41285  lcfrlem19  41540  aks4d1p8d1  42057  evlsvvval  42536  fsuppind  42563  mapfzcons  42689  mzpcl34  42704  mzpindd  42719  mzpsubst  42721  diophrw  42732  diophren  42786  irrapxlem1  42795  pellexlem5  42806  acongrep  42953  pwssplit4  43062  omlimcl2  43215  onexoegt  43217  oasubex  43259  omlim2  43272  nnoeomeqom  43285  nnawordexg  43300  succlg  43301  oacl2g  43303  onmcl  43304  omabs2  43305  omcl2  43306  tfsconcatrev  43321  ofoafg  43327  ofoaf  43328  ofoaass  43333  naddcnfass  43342  naddwordnexlem4  43374  omssrncard  43513  brtrclfv2  43700  rfovcnvf1od  43977  ntrk0kbimka  44012  isotone1  44021  isotone2  44022  4an4132  44473  modelaxrep  44955  mulltgt0  45000  fnchoice  45007  3adantlr3  45018  3adantll2  45019  3adantll3  45020  uzwo4  45031  disjf1o  45169  supxrgelem  45317  infleinflem2  45351  xrralrecnnle  45363  supxrunb3  45379  unb2ltle  45395  infrpgernmpt  45445  iooiinicc  45524  iooiinioc  45538  fmuldfeq  45565  mccl  45580  limccog  45602  limcrecl  45611  lptioo1  45614  islpcn  45621  limsupre  45623  neglimc  45629  0ellimcdiv  45631  limclner  45633  climleltrp  45658  climinf3  45698  liminflimsupclim  45789  xlimpnfxnegmnf  45796  icccncfext  45869  fprodcncf  45882  dvnmptdivc  45920  dvnmul  45925  dvmptfprod  45927  dvnprodlem3  45930  stoweidlem25  46007  stoweidlem34  46016  stoweidlem38  46020  stoweidlem44  46026  stoweidlem48  46030  stoweidlem49  46031  stoweidlem59  46041  stoweidlem60  46042  wallispilem4  46050  stirlinglem5  46060  dirkercncflem2  46086  fourierdlem39  46128  fourierdlem42  46131  fourierdlem46  46134  fourierdlem47  46135  fourierdlem48  46136  fourierdlem50  46138  fourierdlem51  46139  fourierdlem64  46152  fourierdlem73  46161  fourierdlem74  46162  fourierdlem77  46165  fourierdlem80  46168  fourierdlem87  46175  fourierdlem94  46182  fourierdlem103  46191  fourierdlem104  46192  etransclem32  46248  rrxsnicc  46282  sge0cl  46363  sge0f1o  46364  nnfoctbdjlem  46437  ismeannd  46449  omeiunltfirp  46501  hoicvr  46530  ovncvrrp  46546  hoidmvlelem2  46578  hoidmvlelem5  46581  hspdifhsp  46598  hoiqssbllem2  46605  hspmbllem2  46609  vonicclem2  46666  smflimsuplem7  46808  fundcmpsurbijinj  47395  sqrtpwpw2p  47523  lincresunit2  48464  nnpw2pmod  48569  dignn0flhalflem1  48601  dignn0flhalf  48604  rrx2linest  48728  itsclc0yqsol  48750  itsclc0b  48758  brab2dd  48813  oppcendc  49004  imaidfu  49096  imasubc  49137  oppcthinendcALT  49427  functhinclem1  49430  functhinclem2  49431  fullthinc2  49437