Theorem syl21anc 850

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

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

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 401

This theorem is used by:  bibiad  852  syl1111anc  853  rspc2dv  3595  wereu2  5657  frpomin  6341  funtpg  6591  funcnvtp  6599  funcnvqp  6600  fnund  6650  fun2d  6742  fvun1  6972  iinpreima  7064  ftpg  7153  fsnunf  7183  f1prex  7282  soisores  7325  isotr  7334  off  7694  coof  7700  caofrss  7715  caonncan  7720  fvmpocurryd  8265  oaf1o  8546  omeulem1  8565  oeordi  8571  oelimcl  8584  oeeulem  8585  oeeui  8586  oaabs2  8633  omabs  8635  coflton  8655  pmresg  8866  ralxpmap  8892  domunsncan  9063  sucdom2  9185  unxpdom2  9218  sucxpdom  9219  unblem4  9253  fodomfi  9270  hartogslem1  9502  cantnflt  9639  cantnflem3  9658  cantnflem4  9659  cnfcomlem  9666  cnfcom  9667  ttrcltr  9683  infxpenlem  10004  infxpenc  10009  fseqenlem1  10015  pwsdompw  10193  cfeq0  10246  cofsmo  10259  cfsmolem  10260  ssfin4  10300  hsmexlem4  10419  hsmexlem5  10420  axdc3lem2  10441  fpwwe2  10634  wunpr  10700  mulclpi  10884  mulcanenq  10951  distrlem4pr  11017  prlem934  11024  prlem936  11038  divge0d  13106  elfzodif0  13806  elfznelfzob  13810  seqcaopr2  14081  facavg  14344  hashpss  14453  swrdwrdsymb  14707  cats1un  14765  f1oun2prg  14961  sgnsub  15150  sqrtdiv  15323  sqrtdivd  15482  mulcn2  15654  o1of2  15671  fsumsplit  15799  sumsplit  15826  isumless  15906  demoivreALT  16263  rpnnen2lem11  16286  gcdnncl  16571  qredeu  16722  rpdvds  16724  isprm5  16772  rpexp  16787  prmdvdsbc  16791  divnumden  16813  divdenle  16814  phimullem  16844  phisum  16856  pythagtriplem4  16885  pythagtriplem8  16889  pythagtriplem9  16890  pcgcd1  16943  sumhash  16962  fldivp1  16963  pockthlem  16971  setsfun  17237  setsfun0  17238  ssc2  17885  estrreslem1  18199  tleile  18481  chnind  18683  sgrppropd  18795  mndpropd  18823  grpidssd  19088  grpinvssd  19089  issubg2  19214  isnsg3  19232  eqgid  19254  kerf1ghm  19323  ghmqusnsglem1  19356  ghmquskerlem1  19359  ghmqusker  19363  gass  19377  symgextres  19501  gsmsymgreqlem2  19507  sylow1lem5  19678  sylow2alem2  19694  sylow3lem3  19705  efgredlemd  19820  efgredlem  19823  frgpnabllem1  19949  frgpnabllem2  19950  subgdmdprd  20112  ablfacrplem  20143  omndmul3  20210  gsumle  20221  rglcom4d  20299  issrngd  20969  orngmul  20979  lmodprop2d  21056  lsspropd  21149  pwssplit1  21191  lspvadd  21228  drngidl  21396  rhmpreimaidl  21427  isprmidlc  21483  qsidomlem1  21491  qsidomlem2  21492  qsnzr  21494  znidomb  21722  znrrg  21726  lindfind  21977  lindsind  21978  mplsubglem  22159  mplind  22232  evlsvvval  22255  ressply1evl  22541  mat1ghm  22651  mdetunilem1  22780  mdetunilem3  22782  mdetunilem4  22783  mdetunilem9  22788  cramerimplem2  22852  mat2pmatlin  22903  monmatcollpw  22947  cpmadugsumlemF  23044  mretopd  23260  neiptopnei  23300  neitr  23348  ufilen  24098  flimrest  24151  flimclslem  24152  fclsrest  24192  cnextcn  24235  haustsms2  24305  tsmsxplem2  24322  trust  24397  utoptop  24402  restutop  24405  ustuqtop4  24412  utopsnneiplem  24415  utop2nei  24418  utop3cls  24419  isucn2  24446  ucncn  24452  fmucnd  24459  trcfilu  24461  comet  24681  metustexhalf  24724  metustbl  24734  psmetutop  24735  nrmmetd  24742  reconnlem1  24995  reconnlem2  24996  fsumcn  25040  cmetcaulem  25458  iscmet3lem1  25461  iscmet3lem2  25462  bcthlem5  25498  cmslsschl  25547  rrxdstprj1  25579  minveclem4  25602  ovolfiniun  25671  itg1addlem4  25869  itg1addlem5  25870  itgsplitioo  26008  c1liplem1  26166  dvfsumlem1  26196  plyeq0lem  26378  plyn0mulidp  26453  quotcan  26481  psercnlem1  26599  cxplea  26872  birthdaylem3  27129  musumsum  27367  mpodvdsmulf1o  27369  dvdsmulf1o  27371  dchrelbas4  27418  dchrhash  27446  gausslemma2dlem0d  27534  gausslemma2dlem1a  27540  2lgslem1a1  27564  2sqlem8a  27600  2sqlem8  27601  2sqcoprm  27610  2sqmod  27611  chto1ub  27651  vmadivsum  27657  dchrisumlem1  27664  dchrvmasumlem2  27673  dchrvmasumiflem1  27676  rpvmasum2  27687  mulog2sumlem2  27710  selberg2lem  27725  pntrmax  27739  pntpbnd1  27761  pntlemb  27772  pntlemj  27778  noextend  27841  cuteq0  28019  tgjustc1  28755  tgjustc2  28756  ercgrg  28797  motcgr  28816  tglineeltr  28915  colline  28934  miriso  28958  midexlem  28980  perpneq  29005  foot  29013  f1otrg  29231  axcontlem9  29333  uspgr1ewop  29609  nbupgrres  29725  structtocusgr  29807  wlkp1  30040  clwlkl1loop  30143  uspgrn2crct  30168  crctcshwlkn0lem5  30174  3trlond  30535  3pthond  30537  3spthond  30539  frgr3v  30637  vdgn1frgrv2  30658  numclwwlk3  30747  nmblolbii  31162  minvecolem3  31239  minvecolem4  31243  htthlem  31280  bcs2  31545  nmopub2tALT  32272  nmfnleub2  32289  eighmorth  32327  nmophmi  32394  nmopcoadji  32464  hstle  32593  atcvat3i  32759  opreu2reuALT  32834  prssad  32886  prssbd  32887  iinabrex  32925  disjxpin  32944  fmptco1f1o  32989  off2  32997  xppreima2  33007  fgreu  33027  suppovss  33037  1stpreimas  33062  padct  33074  resf1o  33086  fpwrelmap  33089  arginv  33103  argcj  33104  xrofsup  33123  eliccelico  33133  elicoelioo  33134  iocinif  33137  difioo  33138  suppssnn0  33161  elq2  33167  2exple2exp  33189  oexpled  33191  indsupp  33198  indfsid  33200  ccatf1  33278  pfxlsw2ccat  33279  wrdt2ind  33282  ressprs  33295  xrge0addgt0  33346  xrge0adddir  33347  mndlactf1o  33359  mndractf1o  33360  gsumhashmul  33396  gsummulsubdishift1  33397  symgcom  33412  pmtrcnel  33418  pmtrcnel2  33419  pmtrcnelor  33420  cycpmfv2  33443  trsp2cyc  33452  cycpmco2lem7  33461  cyc3genpm  33481  cycpmconjslem2  33484  cyc3conja  33486  archirng  33517  archirngz  33518  rlocf1  33603  rlocisunit  33605  rrgsubm  33613  fracerl  33636  idomsubr  33639  linds2eq  33703  nsgqusf1olem3  33733  lidlunitel  33740  unitpidl1  33741  elrspunidl  33745  mxidlirredi  33763  mxidlirred  33764  qsdrngi  33786  qsdrnglem2  33787  dflring2  33792  rprmasso  33824  1arithidomlem2  33835  1arithufdlem4  33846  zringidom  33850  deg1le0eq0  33872  ply1unit  33874  ply1dg1rt  33879  ply1dg3rt0irred  33883  m1pmeq  33884  selvply1rhmlema  33917  selvply1rhmlem1  33919  evlextv  33941  mplvrpmrhm  33946  esplympl  33966  esplysply  33970  esplyind  33974  esplyindfv  33975  vietadeg1  33977  ply1degltdimlem  34021  ply1degltdim  34022  lindsunlem  34023  lbsdiflsp0  34025  fedgmullem1  34028  fedgmullem2  34029  assalactf1o  34034  ply1annprmidl  34106  minplyirredlem  34109  irngnminplynz  34111  minplyelirng  34114  algextdeglem4  34119  constrconj  34144  constrsqrtcl  34178  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  cos9thpinconstrlem1  34188  1smat1  34203  madjusmdetlem2  34227  qtophaus  34235  locfinref  34240  zarclssn  34272  zar0ring  34277  zarmxt1  34279  rhmpreimacnlem  34283  rhmpreimacn  34284  metideq  34292  sqsscirc2  34308  tpr2rico  34311  fmcncfil  34330  lmxrge0  34351  lmdvg  34352  qqhval2lem  34380  qqhf  34385  qqhnm  34389  esumle  34457  gsumesum  34458  esumlef  34461  esumrnmpt2  34467  esumpcvgval  34477  esum2d  34492  ofcf  34502  ldsysgenld  34559  ldgenpisyslem1  34562  unelros  34570  difelros  34571  inelsros  34577  diffiunisros  34578  imambfm  34661  omssubadd  34699  inelcarsg  34710  carsgsigalem  34714  carsggect  34717  carsgclctunlem2  34718  oddpwdc  34753  eulerpartlems  34759  eulerpartlemb  34767  eulerpartlemt  34770  iwrdsplit  34786  sseqf  34791  sseqfres  34792  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemfrcn0  34929  signsplypnf  34946  signsvtn0  34966  signstfvneq0  34968  signsvtp  34979  signsvtn  34980  fsum2dsub  35003  reprlt  35015  hashreprin  35016  reprgt  35017  reprpmtf1o  35022  chtvalz  35025  breprexplema  35026  breprexplemc  35028  breprexp  35029  circlemeth  35036  logdivsqrle  35046  hgt750lemb  35052  lpadlem3  35077  lpadleft  35082  bnj1536  35251  bnj1001  35356  bnj1280  35417  fineqvnttrclselem2  35543  satffunlem1  35907  satffunlem2  35908  elmrsubrn  36020  neibastop3  36901  finxpsuclem  38071  poimirlem16  38315  poimirlem19  38318  poimirlem20  38319  poimirlem29  38328  mblfinlem3  38338  itg2addnclem3  38352  ftc1cnnclem  38370  lautlt  40893  lautcvr  40894  lauteq  40897  lautco  40899  ltrncl  40927  ltrncnvleN  40932  trljat2  40969  cdlemc6  40998  cdleme20c  41113  cdleme20j  41120  cdleme22e  41146  cdleme22eALTN  41147  cdlemg7aN  41427  cdlemg12e  41449  cdlemg17dALTN  41466  cdlemh  41619  cdlemkfid1N  41723  dibglbN  41968  diblss  41972  diclspsn  41996  dih1  42088  dihglbcpreN  42102  dihmeetlem4preN  42108  lcfrlem19  42363  aks4d1p8d1  42879  fsuppind  43350  mapfzcons  43475  mzpcl34  43490  mzpindd  43505  mzpsubst  43507  diophrw  43518  diophren  43568  irrapxlem1  43577  pellexlem5  43588  acongrep  43735  pwssplit4  43844  omlimcl2  43997  onexoegt  43999  oasubex  44041  omlim2  44054  nnoeomeqom  44067  nnawordexg  44082  succlg  44083  oacl2g  44085  onmcl  44086  omabs2  44087  omcl2  44088  tfsconcatrev  44103  ofoafg  44109  ofoaf  44110  ofoaass  44115  naddcnfass  44124  naddwordnexlem4  44156  omssrncard  44294  brtrclfv2  44481  rfovcnvf1od  44758  ntrk0kbimka  44793  isotone1  44802  isotone2  44803  4an4132  45236  modelaxrep  45718  mulltgt0  45770  fnchoice  45777  3adantlr3  45788  3adantll2  45789  3adantll3  45790  uzwo4  45801  disjf1o  45937  supxrgelem  46081  infleinflem2  46114  xrralrecnnle  46126  supxrunb3  46142  unb2ltle  46157  infrpgernmpt  46207  iooiinicc  46286  iooiinioc  46300  fmuldfeq  46327  mccl  46342  limccog  46364  limcrecl  46373  lptioo1  46376  islpcn  46381  limsupre  46383  neglimc  46389  0ellimcdiv  46391  limclner  46393  climleltrp  46418  climinf3  46458  liminflimsupclim  46549  xlimpnfxnegmnf  46556  icccncfext  46629  fprodcncf  46642  dvnmptdivc  46680  dvnmul  46685  dvmptfprod  46687  dvnprodlem3  46690  stoweidlem25  46767  stoweidlem34  46776  stoweidlem38  46780  stoweidlem44  46786  stoweidlem48  46790  stoweidlem49  46791  stoweidlem59  46801  stoweidlem60  46802  wallispilem4  46810  stirlinglem5  46820  dirkercncflem2  46846  fourierdlem39  46888  fourierdlem42  46891  fourierdlem46  46894  fourierdlem47  46895  fourierdlem48  46896  fourierdlem50  46898  fourierdlem51  46899  fourierdlem64  46912  fourierdlem73  46921  fourierdlem74  46922  fourierdlem77  46925  fourierdlem80  46928  fourierdlem87  46935  fourierdlem94  46942  fourierdlem103  46951  fourierdlem104  46952  etransclem32  47008  rrxsnicc  47042  sge0cl  47123  sge0f1o  47124  nnfoctbdjlem  47197  ismeannd  47209  omeiunltfirp  47261  ovncvrrp  47306  hoidmvlelem2  47338  hoidmvlelem5  47341  hspdifhsp  47358  hoiqssbllem2  47365  hspmbllem2  47369  vonicclem2  47426  smflimsuplem7  47568  fundcmpsurbijinj  48187  sqrtpwpw2p  48318  lincresunit2  49286  nnpw2pmod  49391  dignn0flhalflem1  49423  dignn0flhalf  49426  rrx2linest  49550  itsclc0yqsol  49572  itsclc0b  49580  brab2dd  49634  oppcendc  49824  imaidfu  49916  imasubc  49957  oppcthinendcALT  50247  functhinclem1  50250  functhinclem2  50251  fullthinc2  50257