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  3606  wereu2  5638  frpomin  6316  funtpg  6574  funcnvtp  6582  funcnvqp  6583  fnund  6636  fun2d  6727  fvun1  6955  iinpreima  7044  ftpg  7131  fsnunf  7162  f1prex  7262  soisores  7305  isotr  7314  off  7674  coof  7680  caofrss  7695  caonncan  7700  fvmpocurryd  8253  oaf1o  8530  omeulem1  8549  oeordi  8554  oelimcl  8567  oeeulem  8568  oeeui  8569  oaabs2  8616  omabs  8618  coflton  8638  pmresg  8846  ralxpmap  8872  domunsncan  9046  sucdom2OLD  9056  sucdom2  9173  unxpdom2  9208  sucxpdom  9209  unblem4  9249  fodomfi  9268  fodomfiOLD  9288  hartogslem1  9502  cantnflt  9632  cantnflem3  9651  cantnflem4  9652  cnfcomlem  9659  cnfcom  9660  ttrcltr  9676  infxpenlem  9973  infxpenc  9978  fseqenlem1  9984  pwsdompw  10163  cfeq0  10216  cofsmo  10229  cfsmolem  10230  ssfin4  10270  hsmexlem4  10389  hsmexlem5  10390  axdc3lem2  10411  fpwwe2  10603  wunpr  10669  mulclpi  10853  mulcanenq  10920  distrlem4pr  10986  prlem934  10993  prlem936  11007  divge0d  13042  elfznelfzob  13741  seqcaopr2  14010  facavg  14273  swrdwrdsymb  14634  cats1un  14693  f1oun2prg  14890  sqrtdiv  15238  sqrtdivd  15397  mulcn2  15569  o1of2  15586  fsumsplit  15714  sumsplit  15741  isumless  15818  demoivreALT  16176  rpnnen2lem11  16199  gcdnncl  16484  qredeu  16635  rpdvds  16637  isprm5  16684  rpexp  16699  prmdvdsbc  16703  divnumden  16725  divdenle  16726  phimullem  16756  phisum  16768  pythagtriplem4  16797  pythagtriplem8  16801  pythagtriplem9  16802  pcgcd1  16855  sumhash  16874  fldivp1  16875  pockthlem  16883  setsfun  17148  setsfun0  17149  ssc2  17791  estrreslem1  18105  tleile  18387  sgrppropd  18665  mndpropd  18693  grpidssd  18955  grpinvssd  18956  issubg2  19080  isnsg3  19099  eqgid  19119  kerf1ghm  19186  ghmqusnsglem1  19219  ghmquskerlem1  19222  ghmqusker  19226  gass  19240  symgextres  19362  gsmsymgreqlem2  19368  sylow1lem5  19539  sylow2alem2  19555  sylow3lem3  19566  efgredlemd  19681  efgredlem  19684  frgpnabllem1  19810  frgpnabllem2  19811  subgdmdprd  19973  ablfacrplem  20004  rglcom4d  20127  issrngd  20771  lmodprop2d  20837  lsspropd  20931  pwssplit1  20973  lspvadd  21010  rhmpreimaidl  21194  znidomb  21478  znrrg  21482  lindfind  21732  lindsind  21733  mplsubglem  21915  mplind  21984  ressply1evl  22264  mat1ghm  22377  mdetunilem1  22506  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  cramerimplem2  22578  mat2pmatlin  22629  monmatcollpw  22673  cpmadugsumlemF  22770  mretopd  22986  neiptopnei  23026  neitr  23074  ufilen  23824  flimrest  23877  flimclslem  23878  fclsrest  23918  cnextcn  23961  haustsms2  24031  tsmsxplem2  24048  trust  24124  utoptop  24129  restutop  24132  ustuqtop4  24139  utopsnneiplem  24142  utop2nei  24145  utop3cls  24146  isucn2  24173  ucncn  24179  fmucnd  24186  trcfilu  24188  comet  24408  metustexhalf  24451  metustbl  24461  psmetutop  24462  nrmmetd  24469  reconnlem1  24722  reconnlem2  24723  fsumcn  24768  cmetcaulem  25195  iscmet3lem1  25198  iscmet3lem2  25199  bcthlem5  25235  cmslsschl  25284  rrxdstprj1  25316  minveclem4  25339  ovolfiniun  25409  itg1addlem4  25607  itg1addlem5  25608  itgsplitioo  25746  c1liplem1  25908  dvfsumlem1  25939  plyeq0lem  26122  quotcan  26224  psercnlem1  26342  cxplea  26612  birthdaylem3  26870  musumsum  27109  mpodvdsmulf1o  27111  dvdsmulf1o  27113  dchrelbas4  27161  dchrhash  27189  gausslemma2dlem0d  27277  gausslemma2dlem1a  27283  2lgslem1a1  27307  2sqlem8a  27343  2sqlem8  27344  2sqcoprm  27353  2sqmod  27354  chto1ub  27394  vmadivsum  27400  dchrisumlem1  27407  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  rpvmasum2  27430  mulog2sumlem2  27453  selberg2lem  27468  pntrmax  27482  pntpbnd1  27504  pntlemb  27515  pntlemj  27521  noextend  27585  cuteq0  27751  tgjustc1  28409  tgjustc2  28410  ercgrg  28451  motcgr  28470  tglineeltr  28565  colline  28583  miriso  28604  midexlem  28626  perpneq  28648  foot  28656  f1otrg  28805  axcontlem9  28906  uspgr1ewop  29182  nbupgrres  29298  structtocusgr  29380  wlkp1  29616  clwlkl1loop  29720  uspgrn2crct  29745  crctcshwlkn0lem5  29751  3trlond  30109  3pthond  30111  3spthond  30113  frgr3v  30211  vdgn1frgrv2  30232  numclwwlk3  30321  nmblolbii  30735  minvecolem3  30812  minvecolem4  30816  htthlem  30853  bcs2  31118  nmopub2tALT  31845  nmfnleub2  31862  eighmorth  31900  nmophmi  31967  nmopcoadji  32037  hstle  32166  atcvat3i  32332  opreu2reuALT  32413  prssad  32465  prssbd  32466  iinabrex  32505  disjxpin  32524  fmptco1f1o  32564  off2  32572  xppreima2  32582  fgreu  32603  suppovss  32611  1stpreimas  32636  padct  32650  resf1o  32660  fpwrelmap  32663  arginv  32678  argcj  32679  xrofsup  32697  eliccelico  32707  elicoelioo  32708  iocinif  32711  difioo  32712  elfzodif0  32724  suppssnn0  32737  hashpss  32741  elq2  32743  sgnsub  32769  2exple2exp  32777  oexpled  32779  indsupp  32797  ccatf1  32877  pfxlsw2ccat  32879  wrdt2ind  32882  ressprs  32897  chnind  32944  xrge0addgt0  32965  xrge0adddir  32966  mndlactf1o  32978  mndractf1o  32979  gsumhashmul  33008  omndmul3  33034  gsumle  33045  symgcom  33047  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  cycpmfv2  33078  trsp2cyc  33087  cycpmco2lem7  33096  cyc3genpm  33116  cycpmconjslem2  33119  cyc3conja  33121  archirng  33149  archirngz  33150  rlocf1  33231  rrgsubm  33241  fracerl  33263  idomsubr  33266  orngmul  33288  linds2eq  33359  nsgqusf1olem3  33393  lidlunitel  33401  unitpidl1  33402  elrspunidl  33406  drngidl  33411  isprmidlc  33425  qsidomlem1  33430  qsidomlem2  33431  qsnzr  33433  mxidlirredi  33449  mxidlirred  33450  qsdrngi  33473  qsdrnglem2  33474  rprmasso  33503  1arithidomlem2  33514  1arithufdlem4  33525  zringidom  33529  deg1le0eq0  33549  ply1unit  33551  ply1dg1rt  33555  ply1dg3rt0irred  33558  m1pmeq  33559  ply1degltdimlem  33625  ply1degltdim  33626  lindsunlem  33627  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  assalactf1o  33638  ply1annprmidl  33704  minplyirredlem  33707  irngnminplynz  33709  minplyelirng  33712  algextdeglem4  33717  constrconj  33742  constrsqrtcl  33776  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpinconstrlem1  33786  1smat1  33801  madjusmdetlem2  33825  qtophaus  33833  locfinref  33838  zarclssn  33870  zar0ring  33875  zarmxt1  33877  rhmpreimacnlem  33881  rhmpreimacn  33882  metideq  33890  sqsscirc2  33906  tpr2rico  33909  fmcncfil  33928  lmxrge0  33949  lmdvg  33950  qqhval2lem  33978  qqhf  33983  qqhnm  33987  esumle  34055  gsumesum  34056  esumlef  34059  esumrnmpt2  34065  esumpcvgval  34075  esum2d  34090  ofcf  34100  ldsysgenld  34157  ldgenpisyslem1  34160  unelros  34168  difelros  34169  inelsros  34175  diffiunisros  34176  imambfm  34260  omssubadd  34298  inelcarsg  34309  carsgsigalem  34313  carsggect  34316  carsgclctunlem2  34317  oddpwdc  34352  eulerpartlems  34358  eulerpartlemb  34366  eulerpartlemt  34369  iwrdsplit  34385  sseqf  34390  sseqfres  34391  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemfrcn0  34528  plymulx0  34545  signsplypnf  34548  signsvtn0  34568  signstfvneq0  34570  signsvtp  34581  signsvtn  34582  fsum2dsub  34605  reprlt  34617  hashreprin  34618  reprgt  34619  reprpmtf1o  34624  chtvalz  34627  breprexplema  34628  breprexplemc  34630  breprexp  34631  circlemeth  34638  logdivsqrle  34648  hgt750lemb  34654  lpadlem3  34676  lpadleft  34681  bnj1536  34851  bnj1001  34956  bnj1280  35017  satffunlem1  35401  satffunlem2  35402  elmrsubrn  35514  neibastop3  36357  finxpsuclem  37392  poimirlem16  37637  poimirlem19  37640  poimirlem20  37641  poimirlem29  37650  mblfinlem3  37660  itg2addnclem3  37674  ftc1cnnclem  37692  lautlt  40092  lautcvr  40093  lauteq  40096  lautco  40098  ltrncl  40126  ltrncnvleN  40131  trljat2  40168  cdlemc6  40197  cdleme20c  40312  cdleme20j  40319  cdleme22e  40345  cdleme22eALTN  40346  cdlemg7aN  40626  cdlemg12e  40648  cdlemg17dALTN  40665  cdlemh  40818  cdlemkfid1N  40922  dibglbN  41167  diblss  41171  diclspsn  41195  dih1  41287  dihglbcpreN  41301  dihmeetlem4preN  41307  lcfrlem19  41562  aks4d1p8d1  42079  evlsvvval  42558  fsuppind  42585  mapfzcons  42711  mzpcl34  42726  mzpindd  42741  mzpsubst  42743  diophrw  42754  diophren  42808  irrapxlem1  42817  pellexlem5  42828  acongrep  42976  pwssplit4  43085  omlimcl2  43238  onexoegt  43240  oasubex  43282  omlim2  43295  nnoeomeqom  43308  nnawordexg  43323  succlg  43324  oacl2g  43326  onmcl  43327  omabs2  43328  omcl2  43329  tfsconcatrev  43344  ofoafg  43350  ofoaf  43351  ofoaass  43356  naddcnfass  43365  naddwordnexlem4  43397  omssrncard  43536  brtrclfv2  43723  rfovcnvf1od  44000  ntrk0kbimka  44035  isotone1  44044  isotone2  44045  4an4132  44496  modelaxrep  44978  mulltgt0  45023  fnchoice  45030  3adantlr3  45041  3adantll2  45042  3adantll3  45043  uzwo4  45054  disjf1o  45192  supxrgelem  45340  infleinflem2  45374  xrralrecnnle  45386  supxrunb3  45402  unb2ltle  45418  infrpgernmpt  45468  iooiinicc  45547  iooiinioc  45561  fmuldfeq  45588  mccl  45603  limccog  45625  limcrecl  45634  lptioo1  45637  islpcn  45644  limsupre  45646  neglimc  45652  0ellimcdiv  45654  limclner  45656  climleltrp  45681  climinf3  45721  liminflimsupclim  45812  xlimpnfxnegmnf  45819  icccncfext  45892  fprodcncf  45905  dvnmptdivc  45943  dvnmul  45948  dvmptfprod  45950  dvnprodlem3  45953  stoweidlem25  46030  stoweidlem34  46039  stoweidlem38  46043  stoweidlem44  46049  stoweidlem48  46053  stoweidlem49  46054  stoweidlem59  46064  stoweidlem60  46065  wallispilem4  46073  stirlinglem5  46083  dirkercncflem2  46109  fourierdlem39  46151  fourierdlem42  46154  fourierdlem46  46157  fourierdlem47  46158  fourierdlem48  46159  fourierdlem50  46161  fourierdlem51  46162  fourierdlem64  46175  fourierdlem73  46184  fourierdlem74  46185  fourierdlem77  46188  fourierdlem80  46191  fourierdlem87  46198  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  etransclem32  46271  rrxsnicc  46305  sge0cl  46386  sge0f1o  46387  nnfoctbdjlem  46460  ismeannd  46472  omeiunltfirp  46524  hoicvr  46553  ovncvrrp  46569  hoidmvlelem2  46601  hoidmvlelem5  46604  hspdifhsp  46621  hoiqssbllem2  46628  hspmbllem2  46632  vonicclem2  46689  smflimsuplem7  46831  fundcmpsurbijinj  47415  sqrtpwpw2p  47543  lincresunit2  48471  nnpw2pmod  48576  dignn0flhalflem1  48608  dignn0flhalf  48611  rrx2linest  48735  itsclc0yqsol  48757  itsclc0b  48765  brab2dd  48820  oppcendc  49011  imaidfu  49103  imasubc  49144  oppcthinendcALT  49434  functhinclem1  49437  functhinclem2  49438  fullthinc2  49444