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 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bibiad  852  syl1111anc  853  rspc2dv  3595  wereu2  5658  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  7692  coof  7698  caofrss  7713  caonncan  7718  fvmpocurryd  8266  oaf1o  8547  omeulem1  8566  oeordi  8572  oelimcl  8585  oeeulem  8586  oeeui  8587  oaabs2  8634  omabs  8636  coflton  8656  pmresg  8867  ralxpmap  8893  domunsncan  9064  sucdom2  9186  unxpdom2  9219  sucxpdom  9220  unblem4  9254  fodomfi  9271  hartogslem1  9503  cantnflt  9640  cantnflem3  9659  cantnflem4  9660  cnfcomlem  9667  cnfcom  9668  ttrcltr  9684  infxpenlem  9996  infxpenc  10001  fseqenlem1  10007  pwsdompw  10185  cfeq0  10239  cofsmo  10252  cfsmolem  10253  ssfin4  10293  hsmexlem4  10412  hsmexlem5  10413  axdc3lem2  10434  fpwwe2  10627  wunpr  10693  mulclpi  10877  mulcanenq  10944  distrlem4pr  11010  prlem934  11017  prlem936  11031  divge0d  13099  elfzodif0  13798  elfznelfzob  13802  seqcaopr2  14073  facavg  14336  hashpss  14445  swrdwrdsymb  14699  cats1un  14757  f1oun2prg  14953  sgnsub  15142  sqrtdiv  15315  sqrtdivd  15474  mulcn2  15646  o1of2  15663  fsumsplit  15791  sumsplit  15818  isumless  15898  demoivreALT  16256  rpnnen2lem11  16279  gcdnncl  16564  qredeu  16715  rpdvds  16717  isprm5  16765  rpexp  16780  prmdvdsbc  16784  divnumden  16806  divdenle  16807  phimullem  16837  phisum  16849  pythagtriplem4  16878  pythagtriplem8  16882  pythagtriplem9  16883  pcgcd1  16936  sumhash  16955  fldivp1  16956  pockthlem  16964  setsfun  17230  setsfun0  17231  ssc2  17878  estrreslem1  18192  tleile  18474  chnind  18676  sgrppropd  18788  mndpropd  18816  grpidssd  19081  grpinvssd  19082  issubg2  19207  isnsg3  19225  eqgid  19247  kerf1ghm  19316  ghmqusnsglem1  19349  ghmquskerlem1  19352  ghmqusker  19356  gass  19370  symgextres  19494  gsmsymgreqlem2  19500  sylow1lem5  19671  sylow2alem2  19687  sylow3lem3  19698  efgredlemd  19813  efgredlem  19816  frgpnabllem1  19942  frgpnabllem2  19943  subgdmdprd  20105  ablfacrplem  20136  omndmul3  20203  gsumle  20214  rglcom4d  20292  issrngd  20937  orngmul  20947  lmodprop2d  21024  lsspropd  21117  pwssplit1  21159  lspvadd  21196  drngidl  21364  rhmpreimaidl  21395  isprmidlc  21451  qsidomlem1  21459  qsidomlem2  21460  qsnzr  21462  znidomb  21690  znrrg  21694  lindfind  21945  lindsind  21946  mplsubglem  22127  mplind  22200  evlsvvval  22223  ressply1evl  22509  mat1ghm  22619  mdetunilem1  22748  mdetunilem3  22750  mdetunilem4  22751  mdetunilem9  22756  cramerimplem2  22820  mat2pmatlin  22871  monmatcollpw  22915  cpmadugsumlemF  23012  mretopd  23228  neiptopnei  23268  neitr  23316  ufilen  24066  flimrest  24119  flimclslem  24120  fclsrest  24160  cnextcn  24203  haustsms2  24273  tsmsxplem2  24290  trust  24365  utoptop  24370  restutop  24373  ustuqtop4  24380  utopsnneiplem  24383  utop2nei  24386  utop3cls  24387  isucn2  24414  ucncn  24420  fmucnd  24427  trcfilu  24429  comet  24649  metustexhalf  24692  metustbl  24702  psmetutop  24703  nrmmetd  24710  reconnlem1  24963  reconnlem2  24964  fsumcn  25008  cmetcaulem  25426  iscmet3lem1  25429  iscmet3lem2  25430  bcthlem5  25466  cmslsschl  25515  rrxdstprj1  25547  minveclem4  25570  ovolfiniun  25639  itg1addlem4  25837  itg1addlem5  25838  itgsplitioo  25976  c1liplem1  26134  dvfsumlem1  26164  plyeq0lem  26346  plyn0mulidp  26421  quotcan  26449  psercnlem1  26564  cxplea  26837  birthdaylem3  27094  musumsum  27332  mpodvdsmulf1o  27334  dvdsmulf1o  27336  dchrelbas4  27383  dchrhash  27411  gausslemma2dlem0d  27499  gausslemma2dlem1a  27505  2lgslem1a1  27529  2sqlem8a  27565  2sqlem8  27566  2sqcoprm  27575  2sqmod  27576  chto1ub  27616  vmadivsum  27622  dchrisumlem1  27629  dchrvmasumlem2  27638  dchrvmasumiflem1  27641  rpvmasum2  27652  mulog2sumlem2  27675  selberg2lem  27690  pntrmax  27704  pntpbnd1  27726  pntlemb  27737  pntlemj  27743  noextend  27806  cuteq0  27984  tgjustc1  28720  tgjustc2  28721  ercgrg  28762  motcgr  28781  tglineeltr  28880  colline  28899  miriso  28923  midexlem  28945  perpneq  28969  foot  28977  f1otrg  29186  axcontlem9  29288  uspgr1ewop  29564  nbupgrres  29680  structtocusgr  29762  wlkp1  29995  clwlkl1loop  30098  uspgrn2crct  30123  crctcshwlkn0lem5  30129  3trlond  30490  3pthond  30492  3spthond  30494  frgr3v  30592  vdgn1frgrv2  30613  numclwwlk3  30702  nmblolbii  31117  minvecolem3  31194  minvecolem4  31198  htthlem  31235  bcs2  31500  nmopub2tALT  32227  nmfnleub2  32244  eighmorth  32282  nmophmi  32349  nmopcoadji  32419  hstle  32548  atcvat3i  32714  opreu2reuALT  32789  prssad  32841  prssbd  32842  iinabrex  32880  disjxpin  32899  fmptco1f1o  32944  off2  32952  xppreima2  32962  fgreu  32982  suppovss  32992  1stpreimas  33017  padct  33029  resf1o  33041  fpwrelmap  33044  arginv  33058  argcj  33059  xrofsup  33078  eliccelico  33088  elicoelioo  33089  iocinif  33092  difioo  33093  suppssnn0  33116  elq2  33122  2exple2exp  33144  oexpled  33146  indsupp  33153  indfsid  33155  ccatf1  33235  pfxlsw2ccat  33236  wrdt2ind  33239  ressprs  33252  xrge0addgt0  33303  xrge0adddir  33304  mndlactf1o  33316  mndractf1o  33317  gsumhashmul  33353  gsummulsubdishift1  33354  symgcom  33369  pmtrcnel  33375  pmtrcnel2  33376  pmtrcnelor  33377  cycpmfv2  33400  trsp2cyc  33409  cycpmco2lem7  33418  cyc3genpm  33438  cycpmconjslem2  33441  cyc3conja  33443  archirng  33474  archirngz  33475  rlocf1  33560  rlocisunit  33562  rrgsubm  33570  fracerl  33593  idomsubr  33596  linds2eq  33660  nsgqusf1olem3  33690  lidlunitel  33697  unitpidl1  33698  elrspunidl  33702  mxidlirredi  33720  mxidlirred  33721  qsdrngi  33743  qsdrnglem2  33744  dflring2  33749  rprmasso  33781  1arithidomlem2  33792  1arithufdlem4  33803  zringidom  33807  deg1le0eq0  33829  ply1unit  33831  ply1dg1rt  33836  ply1dg3rt0irred  33840  m1pmeq  33841  selvply1rhmlema  33874  selvply1rhmlem1  33876  evlextv  33898  mplvrpmrhm  33903  esplympl  33923  esplysply  33927  esplyind  33931  esplyindfv  33932  vietadeg1  33934  ply1degltdimlem  33978  ply1degltdim  33979  lindsunlem  33980  lbsdiflsp0  33982  fedgmullem1  33985  fedgmullem2  33986  assalactf1o  33991  ply1annprmidl  34063  minplyirredlem  34066  irngnminplynz  34068  minplyelirng  34071  algextdeglem4  34076  constrconj  34101  constrsqrtcl  34135  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  cos9thpinconstrlem1  34145  1smat1  34160  madjusmdetlem2  34184  qtophaus  34192  locfinref  34197  zarclssn  34229  zar0ring  34234  zarmxt1  34236  rhmpreimacnlem  34240  rhmpreimacn  34241  metideq  34249  sqsscirc2  34265  tpr2rico  34268  fmcncfil  34287  lmxrge0  34308  lmdvg  34309  qqhval2lem  34337  qqhf  34342  qqhnm  34346  esumle  34414  gsumesum  34415  esumlef  34418  esumrnmpt2  34424  esumpcvgval  34434  esum2d  34449  ofcf  34459  ldsysgenld  34516  ldgenpisyslem1  34519  unelros  34527  difelros  34528  inelsros  34534  diffiunisros  34535  imambfm  34618  omssubadd  34656  inelcarsg  34667  carsgsigalem  34671  carsggect  34674  carsgclctunlem2  34675  oddpwdc  34710  eulerpartlems  34716  eulerpartlemb  34724  eulerpartlemt  34727  iwrdsplit  34743  sseqf  34748  sseqfres  34749  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemfrcn0  34886  signsplypnf  34903  signsvtn0  34923  signstfvneq0  34925  signsvtp  34936  signsvtn  34937  fsum2dsub  34960  reprlt  34972  hashreprin  34973  reprgt  34974  reprpmtf1o  34979  chtvalz  34982  breprexplema  34983  breprexplemc  34985  breprexp  34986  circlemeth  34993  logdivsqrle  35003  hgt750lemb  35009  lpadlem3  35034  lpadleft  35039  bnj1536  35208  bnj1001  35313  bnj1280  35374  fineqvnttrclselem2  35489  satffunlem1  35853  satffunlem2  35854  elmrsubrn  35966  neibastop3  36817  finxpsuclem  37987  poimirlem16  38231  poimirlem19  38234  poimirlem20  38235  poimirlem29  38244  mblfinlem3  38254  itg2addnclem3  38268  ftc1cnnclem  38286  lautlt  40811  lautcvr  40812  lauteq  40815  lautco  40817  ltrncl  40845  ltrncnvleN  40850  trljat2  40887  cdlemc6  40916  cdleme20c  41031  cdleme20j  41038  cdleme22e  41064  cdleme22eALTN  41065  cdlemg7aN  41345  cdlemg12e  41367  cdlemg17dALTN  41384  cdlemh  41537  cdlemkfid1N  41641  dibglbN  41886  diblss  41890  diclspsn  41914  dih1  42006  dihglbcpreN  42020  dihmeetlem4preN  42026  lcfrlem19  42281  aks4d1p8d1  42797  fsuppind  43270  mapfzcons  43395  mzpcl34  43410  mzpindd  43425  mzpsubst  43427  diophrw  43438  diophren  43488  irrapxlem1  43497  pellexlem5  43508  acongrep  43655  pwssplit4  43764  omlimcl2  43917  onexoegt  43919  oasubex  43961  omlim2  43974  nnoeomeqom  43987  nnawordexg  44002  succlg  44003  oacl2g  44005  onmcl  44006  omabs2  44007  omcl2  44008  tfsconcatrev  44023  ofoafg  44029  ofoaf  44030  ofoaass  44035  naddcnfass  44044  naddwordnexlem4  44076  omssrncard  44214  brtrclfv2  44401  rfovcnvf1od  44678  ntrk0kbimka  44713  isotone1  44722  isotone2  44723  4an4132  45156  modelaxrep  45638  mulltgt0  45690  fnchoice  45697  3adantlr3  45708  3adantll2  45709  3adantll3  45710  uzwo4  45721  disjf1o  45857  supxrgelem  46001  infleinflem2  46034  xrralrecnnle  46046  supxrunb3  46062  unb2ltle  46077  infrpgernmpt  46127  iooiinicc  46206  iooiinioc  46220  fmuldfeq  46247  mccl  46262  limccog  46284  limcrecl  46293  lptioo1  46296  islpcn  46301  limsupre  46303  neglimc  46309  0ellimcdiv  46311  limclner  46313  climleltrp  46338  climinf3  46378  liminflimsupclim  46469  xlimpnfxnegmnf  46476  icccncfext  46549  fprodcncf  46562  dvnmptdivc  46600  dvnmul  46605  dvmptfprod  46607  dvnprodlem3  46610  stoweidlem25  46687  stoweidlem34  46696  stoweidlem38  46700  stoweidlem44  46706  stoweidlem48  46710  stoweidlem49  46711  stoweidlem59  46721  stoweidlem60  46722  wallispilem4  46730  stirlinglem5  46740  dirkercncflem2  46766  fourierdlem39  46808  fourierdlem42  46811  fourierdlem46  46814  fourierdlem47  46815  fourierdlem48  46816  fourierdlem50  46818  fourierdlem51  46819  fourierdlem64  46832  fourierdlem73  46841  fourierdlem74  46842  fourierdlem77  46845  fourierdlem80  46848  fourierdlem87  46855  fourierdlem94  46862  fourierdlem103  46871  fourierdlem104  46872  etransclem32  46928  rrxsnicc  46962  sge0cl  47043  sge0f1o  47044  nnfoctbdjlem  47117  ismeannd  47129  omeiunltfirp  47181  ovncvrrp  47226  hoidmvlelem2  47258  hoidmvlelem5  47261  hspdifhsp  47278  hoiqssbllem2  47285  hspmbllem2  47289  vonicclem2  47346  smflimsuplem7  47488  fundcmpsurbijinj  48104  sqrtpwpw2p  48235  lincresunit2  49203  nnpw2pmod  49308  dignn0flhalflem1  49340  dignn0flhalf  49343  rrx2linest  49467  itsclc0yqsol  49489  itsclc0b  49497  brab2dd  49551  oppcendc  49741  imaidfu  49833  imasubc  49874  oppcthinendcALT  50164  functhinclem1  50167  functhinclem2  50168  fullthinc2  50174