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  3592  wereu2  5613  frpomin  6287  funtpg  6536  funcnvtp  6544  funcnvqp  6545  fnund  6596  fun2d  6687  fvun1  6913  iinpreima  7002  ftpg  7089  fsnunf  7119  f1prex  7218  soisores  7261  isotr  7270  off  7628  coof  7634  caofrss  7649  caonncan  7654  fvmpocurryd  8201  oaf1o  8478  omeulem1  8497  oeordi  8502  oelimcl  8515  oeeulem  8516  oeeui  8517  oaabs2  8564  omabs  8566  coflton  8586  pmresg  8794  ralxpmap  8820  domunsncan  8990  sucdom2  9112  unxpdom2  9144  sucxpdom  9145  unblem4  9179  fodomfi  9196  fodomfiOLD  9214  hartogslem1  9428  cantnflt  9562  cantnflem3  9581  cantnflem4  9582  cnfcomlem  9589  cnfcom  9590  ttrcltr  9606  infxpenlem  9901  infxpenc  9906  fseqenlem1  9912  pwsdompw  10091  cfeq0  10144  cofsmo  10157  cfsmolem  10158  ssfin4  10198  hsmexlem4  10317  hsmexlem5  10318  axdc3lem2  10339  fpwwe2  10531  wunpr  10597  mulclpi  10781  mulcanenq  10848  distrlem4pr  10914  prlem934  10921  prlem936  10935  divge0d  12971  elfzodif0  13667  elfznelfzob  13671  seqcaopr2  13942  facavg  14205  swrdwrdsymb  14567  cats1un  14625  f1oun2prg  14821  sqrtdiv  15169  sqrtdivd  15328  mulcn2  15500  o1of2  15517  fsumsplit  15645  sumsplit  15672  isumless  15749  demoivreALT  16107  rpnnen2lem11  16130  gcdnncl  16415  qredeu  16566  rpdvds  16568  isprm5  16615  rpexp  16630  prmdvdsbc  16634  divnumden  16656  divdenle  16657  phimullem  16687  phisum  16699  pythagtriplem4  16728  pythagtriplem8  16732  pythagtriplem9  16733  pcgcd1  16786  sumhash  16805  fldivp1  16806  pockthlem  16814  setsfun  17079  setsfun0  17080  ssc2  17726  estrreslem1  18040  tleile  18322  chnind  18524  sgrppropd  18636  mndpropd  18664  grpidssd  18926  grpinvssd  18927  issubg2  19051  isnsg3  19070  eqgid  19090  kerf1ghm  19157  ghmqusnsglem1  19190  ghmquskerlem1  19193  ghmqusker  19197  gass  19211  symgextres  19335  gsmsymgreqlem2  19341  sylow1lem5  19512  sylow2alem2  19528  sylow3lem3  19539  efgredlemd  19654  efgredlem  19657  frgpnabllem1  19783  frgpnabllem2  19784  subgdmdprd  19946  ablfacrplem  19977  omndmul3  20044  gsumle  20055  rglcom4d  20127  issrngd  20768  orngmul  20778  lmodprop2d  20855  lsspropd  20949  pwssplit1  20991  lspvadd  21028  rhmpreimaidl  21212  znidomb  21496  znrrg  21500  lindfind  21751  lindsind  21752  mplsubglem  21934  mplind  22003  ressply1evl  22283  mat1ghm  22396  mdetunilem1  22525  mdetunilem3  22527  mdetunilem4  22528  mdetunilem9  22533  cramerimplem2  22597  mat2pmatlin  22648  monmatcollpw  22692  cpmadugsumlemF  22789  mretopd  23005  neiptopnei  23045  neitr  23093  ufilen  23843  flimrest  23896  flimclslem  23897  fclsrest  23937  cnextcn  23980  haustsms2  24050  tsmsxplem2  24067  trust  24142  utoptop  24147  restutop  24150  ustuqtop4  24157  utopsnneiplem  24160  utop2nei  24163  utop3cls  24164  isucn2  24191  ucncn  24197  fmucnd  24204  trcfilu  24206  comet  24426  metustexhalf  24469  metustbl  24479  psmetutop  24480  nrmmetd  24487  reconnlem1  24740  reconnlem2  24741  fsumcn  24786  cmetcaulem  25213  iscmet3lem1  25216  iscmet3lem2  25217  bcthlem5  25253  cmslsschl  25302  rrxdstprj1  25334  minveclem4  25357  ovolfiniun  25427  itg1addlem4  25625  itg1addlem5  25626  itgsplitioo  25764  c1liplem1  25926  dvfsumlem1  25957  plyeq0lem  26140  quotcan  26242  psercnlem1  26360  cxplea  26630  birthdaylem3  26888  musumsum  27127  mpodvdsmulf1o  27129  dvdsmulf1o  27131  dchrelbas4  27179  dchrhash  27207  gausslemma2dlem0d  27295  gausslemma2dlem1a  27301  2lgslem1a1  27325  2sqlem8a  27361  2sqlem8  27362  2sqcoprm  27371  2sqmod  27372  chto1ub  27412  vmadivsum  27418  dchrisumlem1  27425  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  rpvmasum2  27448  mulog2sumlem2  27471  selberg2lem  27486  pntrmax  27500  pntpbnd1  27522  pntlemb  27533  pntlemj  27539  noextend  27603  cuteq0  27774  tgjustc1  28451  tgjustc2  28452  ercgrg  28493  motcgr  28512  tglineeltr  28607  colline  28625  miriso  28646  midexlem  28668  perpneq  28690  foot  28698  f1otrg  28847  axcontlem9  28948  uspgr1ewop  29224  nbupgrres  29340  structtocusgr  29422  wlkp1  29656  clwlkl1loop  29759  uspgrn2crct  29784  crctcshwlkn0lem5  29790  3trlond  30148  3pthond  30150  3spthond  30152  frgr3v  30250  vdgn1frgrv2  30271  numclwwlk3  30360  nmblolbii  30774  minvecolem3  30851  minvecolem4  30855  htthlem  30892  bcs2  31157  nmopub2tALT  31884  nmfnleub2  31901  eighmorth  31939  nmophmi  32006  nmopcoadji  32076  hstle  32205  atcvat3i  32371  opreu2reuALT  32451  prssad  32504  prssbd  32505  iinabrex  32544  disjxpin  32563  fmptco1f1o  32610  off2  32618  xppreima2  32628  fgreu  32649  suppovss  32657  1stpreimas  32682  padct  32696  resf1o  32708  fpwrelmap  32711  arginv  32726  argcj  32727  xrofsup  32745  eliccelico  32755  elicoelioo  32756  iocinif  32759  difioo  32760  suppssnn0  32782  hashpss  32786  elq2  32789  sgnsub  32815  2exple2exp  32823  oexpled  32825  indsupp  32843  indfsid  32845  ccatf1  32925  pfxlsw2ccat  32926  wrdt2ind  32929  ressprs  32942  xrge0addgt0  32993  xrge0adddir  32994  mndlactf1o  33006  mndractf1o  33007  gsumhashmul  33036  symgcom  33047  pmtrcnel  33053  pmtrcnel2  33054  pmtrcnelor  33055  cycpmfv2  33078  trsp2cyc  33087  cycpmco2lem7  33096  cyc3genpm  33116  cycpmconjslem2  33119  cyc3conja  33121  archirng  33152  archirngz  33153  rlocf1  33235  rrgsubm  33245  fracerl  33267  idomsubr  33270  linds2eq  33341  nsgqusf1olem3  33375  lidlunitel  33383  unitpidl1  33384  elrspunidl  33388  drngidl  33393  isprmidlc  33407  qsidomlem1  33412  qsidomlem2  33413  qsnzr  33415  mxidlirredi  33431  mxidlirred  33432  qsdrngi  33455  qsdrnglem2  33456  rprmasso  33485  1arithidomlem2  33496  1arithufdlem4  33507  zringidom  33511  deg1le0eq0  33531  ply1unit  33533  ply1dg1rt  33538  ply1dg3rt0irred  33541  m1pmeq  33542  mplvrpmrhm  33572  esplympl  33583  esplysply  33587  ply1degltdimlem  33630  ply1degltdim  33631  lindsunlem  33632  lbsdiflsp0  33634  fedgmullem1  33637  fedgmullem2  33638  assalactf1o  33643  ply1annprmidl  33715  minplyirredlem  33718  irngnminplynz  33720  minplyelirng  33723  algextdeglem4  33728  constrconj  33753  constrsqrtcl  33787  cos9thpiminplylem1  33790  cos9thpiminplylem2  33791  cos9thpinconstrlem1  33797  1smat1  33812  madjusmdetlem2  33836  qtophaus  33844  locfinref  33849  zarclssn  33881  zar0ring  33886  zarmxt1  33888  rhmpreimacnlem  33892  rhmpreimacn  33893  metideq  33901  sqsscirc2  33917  tpr2rico  33920  fmcncfil  33939  lmxrge0  33960  lmdvg  33961  qqhval2lem  33989  qqhf  33994  qqhnm  33998  esumle  34066  gsumesum  34067  esumlef  34070  esumrnmpt2  34076  esumpcvgval  34086  esum2d  34101  ofcf  34111  ldsysgenld  34168  ldgenpisyslem1  34171  unelros  34179  difelros  34180  inelsros  34186  diffiunisros  34187  imambfm  34270  omssubadd  34308  inelcarsg  34319  carsgsigalem  34323  carsggect  34326  carsgclctunlem2  34327  oddpwdc  34362  eulerpartlems  34368  eulerpartlemb  34376  eulerpartlemt  34379  iwrdsplit  34395  sseqf  34400  sseqfres  34401  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemfrcn0  34538  plymulx0  34555  signsplypnf  34558  signsvtn0  34578  signstfvneq0  34580  signsvtp  34591  signsvtn  34592  fsum2dsub  34615  reprlt  34627  hashreprin  34628  reprgt  34629  reprpmtf1o  34634  chtvalz  34637  breprexplema  34638  breprexplemc  34640  breprexp  34641  circlemeth  34648  logdivsqrle  34658  hgt750lemb  34664  lpadlem3  34686  lpadleft  34691  bnj1536  34861  bnj1001  34966  bnj1280  35027  fineqvnttrclselem2  35130  satffunlem1  35439  satffunlem2  35440  elmrsubrn  35552  neibastop3  36395  finxpsuclem  37430  poimirlem16  37675  poimirlem19  37678  poimirlem20  37679  poimirlem29  37688  mblfinlem3  37698  itg2addnclem3  37712  ftc1cnnclem  37730  lautlt  40129  lautcvr  40130  lauteq  40133  lautco  40135  ltrncl  40163  ltrncnvleN  40168  trljat2  40205  cdlemc6  40234  cdleme20c  40349  cdleme20j  40356  cdleme22e  40382  cdleme22eALTN  40383  cdlemg7aN  40663  cdlemg12e  40685  cdlemg17dALTN  40702  cdlemh  40855  cdlemkfid1N  40959  dibglbN  41204  diblss  41208  diclspsn  41232  dih1  41324  dihglbcpreN  41338  dihmeetlem4preN  41344  lcfrlem19  41599  aks4d1p8d1  42116  evlsvvval  42595  fsuppind  42622  mapfzcons  42748  mzpcl34  42763  mzpindd  42778  mzpsubst  42780  diophrw  42791  diophren  42845  irrapxlem1  42854  pellexlem5  42865  acongrep  43012  pwssplit4  43121  omlimcl2  43274  onexoegt  43276  oasubex  43318  omlim2  43331  nnoeomeqom  43344  nnawordexg  43359  succlg  43360  oacl2g  43362  onmcl  43363  omabs2  43364  omcl2  43365  tfsconcatrev  43380  ofoafg  43386  ofoaf  43387  ofoaass  43392  naddcnfass  43401  naddwordnexlem4  43433  omssrncard  43572  brtrclfv2  43759  rfovcnvf1od  44036  ntrk0kbimka  44071  isotone1  44080  isotone2  44081  4an4132  44531  modelaxrep  45013  mulltgt0  45058  fnchoice  45065  3adantlr3  45076  3adantll2  45077  3adantll3  45078  uzwo4  45089  disjf1o  45227  supxrgelem  45375  infleinflem2  45408  xrralrecnnle  45420  supxrunb3  45436  unb2ltle  45452  infrpgernmpt  45502  iooiinicc  45581  iooiinioc  45595  fmuldfeq  45622  mccl  45637  limccog  45659  limcrecl  45668  lptioo1  45671  islpcn  45676  limsupre  45678  neglimc  45684  0ellimcdiv  45686  limclner  45688  climleltrp  45713  climinf3  45753  liminflimsupclim  45844  xlimpnfxnegmnf  45851  icccncfext  45924  fprodcncf  45937  dvnmptdivc  45975  dvnmul  45980  dvmptfprod  45982  dvnprodlem3  45985  stoweidlem25  46062  stoweidlem34  46071  stoweidlem38  46075  stoweidlem44  46081  stoweidlem48  46085  stoweidlem49  46086  stoweidlem59  46096  stoweidlem60  46097  wallispilem4  46105  stirlinglem5  46115  dirkercncflem2  46141  fourierdlem39  46183  fourierdlem42  46186  fourierdlem46  46189  fourierdlem47  46190  fourierdlem48  46191  fourierdlem50  46193  fourierdlem51  46194  fourierdlem64  46207  fourierdlem73  46216  fourierdlem74  46217  fourierdlem77  46220  fourierdlem80  46223  fourierdlem87  46230  fourierdlem94  46237  fourierdlem103  46246  fourierdlem104  46247  etransclem32  46303  rrxsnicc  46337  sge0cl  46418  sge0f1o  46419  nnfoctbdjlem  46492  ismeannd  46504  omeiunltfirp  46556  hoicvr  46585  ovncvrrp  46601  hoidmvlelem2  46633  hoidmvlelem5  46636  hspdifhsp  46653  hoiqssbllem2  46660  hspmbllem2  46664  vonicclem2  46721  smflimsuplem7  46863  fundcmpsurbijinj  47440  sqrtpwpw2p  47568  lincresunit2  48509  nnpw2pmod  48614  dignn0flhalflem1  48646  dignn0flhalf  48649  rrx2linest  48773  itsclc0yqsol  48795  itsclc0b  48803  brab2dd  48858  oppcendc  49049  imaidfu  49141  imasubc  49182  oppcthinendcALT  49472  functhinclem1  49475  functhinclem2  49476  fullthinc2  49482