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  3589  wereu2  5618  frpomin  6295  funtpg  6544  funcnvtp  6552  funcnvqp  6553  fnund  6604  fun2d  6695  fvun1  6922  iinpreima  7011  ftpg  7098  fsnunf  7128  f1prex  7227  soisores  7270  isotr  7279  off  7637  coof  7643  caofrss  7658  caonncan  7663  fvmpocurryd  8210  oaf1o  8487  omeulem1  8506  oeordi  8511  oelimcl  8524  oeeulem  8525  oeeui  8526  oaabs2  8573  omabs  8575  coflton  8595  pmresg  8803  ralxpmap  8829  domunsncan  9000  sucdom2  9122  unxpdom2  9154  sucxpdom  9155  unblem4  9189  fodomfi  9206  fodomfiOLD  9224  hartogslem1  9438  cantnflt  9572  cantnflem3  9591  cantnflem4  9592  cnfcomlem  9599  cnfcom  9600  ttrcltr  9616  infxpenlem  9914  infxpenc  9919  fseqenlem1  9925  pwsdompw  10104  cfeq0  10157  cofsmo  10170  cfsmolem  10171  ssfin4  10211  hsmexlem4  10330  hsmexlem5  10331  axdc3lem2  10352  fpwwe2  10544  wunpr  10610  mulclpi  10794  mulcanenq  10861  distrlem4pr  10927  prlem934  10934  prlem936  10948  divge0d  12984  elfzodif0  13680  elfznelfzob  13684  seqcaopr2  13955  facavg  14218  swrdwrdsymb  14580  cats1un  14638  f1oun2prg  14834  sqrtdiv  15182  sqrtdivd  15341  mulcn2  15513  o1of2  15530  fsumsplit  15658  sumsplit  15685  isumless  15762  demoivreALT  16120  rpnnen2lem11  16143  gcdnncl  16428  qredeu  16579  rpdvds  16581  isprm5  16628  rpexp  16643  prmdvdsbc  16647  divnumden  16669  divdenle  16670  phimullem  16700  phisum  16712  pythagtriplem4  16741  pythagtriplem8  16745  pythagtriplem9  16746  pcgcd1  16799  sumhash  16818  fldivp1  16819  pockthlem  16827  setsfun  17092  setsfun0  17093  ssc2  17739  estrreslem1  18053  tleile  18335  chnind  18537  sgrppropd  18649  mndpropd  18677  grpidssd  18939  grpinvssd  18940  issubg2  19064  isnsg3  19082  eqgid  19102  kerf1ghm  19169  ghmqusnsglem1  19202  ghmquskerlem1  19205  ghmqusker  19209  gass  19223  symgextres  19347  gsmsymgreqlem2  19353  sylow1lem5  19524  sylow2alem2  19540  sylow3lem3  19551  efgredlemd  19666  efgredlem  19669  frgpnabllem1  19795  frgpnabllem2  19796  subgdmdprd  19958  ablfacrplem  19989  omndmul3  20056  gsumle  20067  rglcom4d  20139  issrngd  20780  orngmul  20790  lmodprop2d  20867  lsspropd  20961  pwssplit1  21003  lspvadd  21040  rhmpreimaidl  21224  znidomb  21508  znrrg  21512  lindfind  21763  lindsind  21764  mplsubglem  21946  mplind  22015  ressply1evl  22295  mat1ghm  22408  mdetunilem1  22537  mdetunilem3  22539  mdetunilem4  22540  mdetunilem9  22545  cramerimplem2  22609  mat2pmatlin  22660  monmatcollpw  22704  cpmadugsumlemF  22801  mretopd  23017  neiptopnei  23057  neitr  23105  ufilen  23855  flimrest  23908  flimclslem  23909  fclsrest  23949  cnextcn  23992  haustsms2  24062  tsmsxplem2  24079  trust  24154  utoptop  24159  restutop  24162  ustuqtop4  24169  utopsnneiplem  24172  utop2nei  24175  utop3cls  24176  isucn2  24203  ucncn  24209  fmucnd  24216  trcfilu  24218  comet  24438  metustexhalf  24481  metustbl  24491  psmetutop  24492  nrmmetd  24499  reconnlem1  24752  reconnlem2  24753  fsumcn  24798  cmetcaulem  25225  iscmet3lem1  25228  iscmet3lem2  25229  bcthlem5  25265  cmslsschl  25314  rrxdstprj1  25346  minveclem4  25369  ovolfiniun  25439  itg1addlem4  25637  itg1addlem5  25638  itgsplitioo  25776  c1liplem1  25938  dvfsumlem1  25969  plyeq0lem  26152  quotcan  26254  psercnlem1  26372  cxplea  26642  birthdaylem3  26900  musumsum  27139  mpodvdsmulf1o  27141  dvdsmulf1o  27143  dchrelbas4  27191  dchrhash  27219  gausslemma2dlem0d  27307  gausslemma2dlem1a  27313  2lgslem1a1  27337  2sqlem8a  27373  2sqlem8  27374  2sqcoprm  27383  2sqmod  27384  chto1ub  27424  vmadivsum  27430  dchrisumlem1  27437  dchrvmasumlem2  27446  dchrvmasumiflem1  27449  rpvmasum2  27460  mulog2sumlem2  27483  selberg2lem  27498  pntrmax  27512  pntpbnd1  27534  pntlemb  27545  pntlemj  27551  noextend  27615  cuteq0  27786  tgjustc1  28463  tgjustc2  28464  ercgrg  28505  motcgr  28524  tglineeltr  28619  colline  28637  miriso  28658  midexlem  28680  perpneq  28702  foot  28710  f1otrg  28859  axcontlem9  28961  uspgr1ewop  29237  nbupgrres  29353  structtocusgr  29435  wlkp1  29669  clwlkl1loop  29772  uspgrn2crct  29797  crctcshwlkn0lem5  29803  3trlond  30164  3pthond  30166  3spthond  30168  frgr3v  30266  vdgn1frgrv2  30287  numclwwlk3  30376  nmblolbii  30790  minvecolem3  30867  minvecolem4  30871  htthlem  30908  bcs2  31173  nmopub2tALT  31900  nmfnleub2  31917  eighmorth  31955  nmophmi  32022  nmopcoadji  32092  hstle  32221  atcvat3i  32387  opreu2reuALT  32467  prssad  32520  prssbd  32521  iinabrex  32560  disjxpin  32579  fmptco1f1o  32626  off2  32634  xppreima2  32644  fgreu  32665  suppovss  32673  1stpreimas  32698  padct  32712  resf1o  32724  fpwrelmap  32727  arginv  32742  argcj  32743  xrofsup  32761  eliccelico  32771  elicoelioo  32772  iocinif  32775  difioo  32776  suppssnn0  32798  hashpss  32802  elq2  32805  sgnsub  32831  2exple2exp  32839  oexpled  32841  indsupp  32859  indfsid  32861  ccatf1  32941  pfxlsw2ccat  32942  wrdt2ind  32945  ressprs  32958  xrge0addgt0  33009  xrge0adddir  33010  mndlactf1o  33022  mndractf1o  33023  gsumhashmul  33052  symgcom  33063  pmtrcnel  33069  pmtrcnel2  33070  pmtrcnelor  33071  cycpmfv2  33094  trsp2cyc  33103  cycpmco2lem7  33112  cyc3genpm  33132  cycpmconjslem2  33135  cyc3conja  33137  archirng  33168  archirngz  33169  rlocf1  33251  rrgsubm  33261  fracerl  33283  idomsubr  33286  linds2eq  33357  nsgqusf1olem3  33391  lidlunitel  33399  unitpidl1  33400  elrspunidl  33404  drngidl  33409  isprmidlc  33423  qsidomlem1  33428  qsidomlem2  33429  qsnzr  33431  mxidlirredi  33447  mxidlirred  33448  qsdrngi  33471  qsdrnglem2  33472  rprmasso  33501  1arithidomlem2  33512  1arithufdlem4  33523  zringidom  33527  deg1le0eq0  33547  ply1unit  33549  ply1dg1rt  33554  ply1dg3rt0irred  33557  m1pmeq  33558  mplvrpmrhm  33588  esplympl  33599  esplysply  33603  ply1degltdimlem  33646  ply1degltdim  33647  lindsunlem  33648  lbsdiflsp0  33650  fedgmullem1  33653  fedgmullem2  33654  assalactf1o  33659  ply1annprmidl  33731  minplyirredlem  33734  irngnminplynz  33736  minplyelirng  33739  algextdeglem4  33744  constrconj  33769  constrsqrtcl  33803  cos9thpiminplylem1  33806  cos9thpiminplylem2  33807  cos9thpinconstrlem1  33813  1smat1  33828  madjusmdetlem2  33852  qtophaus  33860  locfinref  33865  zarclssn  33897  zar0ring  33902  zarmxt1  33904  rhmpreimacnlem  33908  rhmpreimacn  33909  metideq  33917  sqsscirc2  33933  tpr2rico  33936  fmcncfil  33955  lmxrge0  33976  lmdvg  33977  qqhval2lem  34005  qqhf  34010  qqhnm  34014  esumle  34082  gsumesum  34083  esumlef  34086  esumrnmpt2  34092  esumpcvgval  34102  esum2d  34117  ofcf  34127  ldsysgenld  34184  ldgenpisyslem1  34187  unelros  34195  difelros  34196  inelsros  34202  diffiunisros  34203  imambfm  34286  omssubadd  34324  inelcarsg  34335  carsgsigalem  34339  carsggect  34342  carsgclctunlem2  34343  oddpwdc  34378  eulerpartlems  34384  eulerpartlemb  34392  eulerpartlemt  34395  iwrdsplit  34411  sseqf  34416  sseqfres  34417  ballotlemfc0  34517  ballotlemfcc  34518  ballotlemfrcn0  34554  plymulx0  34571  signsplypnf  34574  signsvtn0  34594  signstfvneq0  34596  signsvtp  34607  signsvtn  34608  fsum2dsub  34631  reprlt  34643  hashreprin  34644  reprgt  34645  reprpmtf1o  34650  chtvalz  34653  breprexplema  34654  breprexplemc  34656  breprexp  34657  circlemeth  34664  logdivsqrle  34674  hgt750lemb  34680  lpadlem3  34702  lpadleft  34707  bnj1536  34877  bnj1001  34982  bnj1280  35043  fineqvnttrclselem2  35153  satffunlem1  35462  satffunlem2  35463  elmrsubrn  35575  neibastop3  36417  finxpsuclem  37452  poimirlem16  37686  poimirlem19  37689  poimirlem20  37690  poimirlem29  37699  mblfinlem3  37709  itg2addnclem3  37723  ftc1cnnclem  37741  lautlt  40200  lautcvr  40201  lauteq  40204  lautco  40206  ltrncl  40234  ltrncnvleN  40239  trljat2  40276  cdlemc6  40305  cdleme20c  40420  cdleme20j  40427  cdleme22e  40453  cdleme22eALTN  40454  cdlemg7aN  40734  cdlemg12e  40756  cdlemg17dALTN  40773  cdlemh  40926  cdlemkfid1N  41030  dibglbN  41275  diblss  41279  diclspsn  41303  dih1  41395  dihglbcpreN  41409  dihmeetlem4preN  41415  lcfrlem19  41670  aks4d1p8d1  42187  evlsvvval  42671  fsuppind  42698  mapfzcons  42823  mzpcl34  42838  mzpindd  42853  mzpsubst  42855  diophrw  42866  diophren  42920  irrapxlem1  42929  pellexlem5  42940  acongrep  43087  pwssplit4  43196  omlimcl2  43349  onexoegt  43351  oasubex  43393  omlim2  43406  nnoeomeqom  43419  nnawordexg  43434  succlg  43435  oacl2g  43437  onmcl  43438  omabs2  43439  omcl2  43440  tfsconcatrev  43455  ofoafg  43461  ofoaf  43462  ofoaass  43467  naddcnfass  43476  naddwordnexlem4  43508  omssrncard  43647  brtrclfv2  43834  rfovcnvf1od  44111  ntrk0kbimka  44146  isotone1  44155  isotone2  44156  4an4132  44606  modelaxrep  45088  mulltgt0  45133  fnchoice  45140  3adantlr3  45151  3adantll2  45152  3adantll3  45153  uzwo4  45164  disjf1o  45302  supxrgelem  45450  infleinflem2  45483  xrralrecnnle  45495  supxrunb3  45511  unb2ltle  45527  infrpgernmpt  45577  iooiinicc  45656  iooiinioc  45670  fmuldfeq  45697  mccl  45712  limccog  45734  limcrecl  45743  lptioo1  45746  islpcn  45751  limsupre  45753  neglimc  45759  0ellimcdiv  45761  limclner  45763  climleltrp  45788  climinf3  45828  liminflimsupclim  45919  xlimpnfxnegmnf  45926  icccncfext  45999  fprodcncf  46012  dvnmptdivc  46050  dvnmul  46055  dvmptfprod  46057  dvnprodlem3  46060  stoweidlem25  46137  stoweidlem34  46146  stoweidlem38  46150  stoweidlem44  46156  stoweidlem48  46160  stoweidlem49  46161  stoweidlem59  46171  stoweidlem60  46172  wallispilem4  46180  stirlinglem5  46190  dirkercncflem2  46216  fourierdlem39  46258  fourierdlem42  46261  fourierdlem46  46264  fourierdlem47  46265  fourierdlem48  46266  fourierdlem50  46268  fourierdlem51  46269  fourierdlem64  46282  fourierdlem73  46291  fourierdlem74  46292  fourierdlem77  46295  fourierdlem80  46298  fourierdlem87  46305  fourierdlem94  46312  fourierdlem103  46321  fourierdlem104  46322  etransclem32  46378  rrxsnicc  46412  sge0cl  46493  sge0f1o  46494  nnfoctbdjlem  46567  ismeannd  46579  omeiunltfirp  46631  hoicvr  46660  ovncvrrp  46676  hoidmvlelem2  46708  hoidmvlelem5  46711  hspdifhsp  46728  hoiqssbllem2  46735  hspmbllem2  46739  vonicclem2  46796  smflimsuplem7  46938  fundcmpsurbijinj  47524  sqrtpwpw2p  47652  lincresunit2  48593  nnpw2pmod  48698  dignn0flhalflem1  48730  dignn0flhalf  48733  rrx2linest  48857  itsclc0yqsol  48879  itsclc0b  48887  brab2dd  48942  oppcendc  49133  imaidfu  49225  imasubc  49266  oppcthinendcALT  49556  functhinclem1  49559  functhinclem2  49560  fullthinc2  49566