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  3588  wereu2  5616  frpomin  6292  funtpg  6541  funcnvtp  6549  funcnvqp  6550  fnund  6601  fun2d  6692  fvun1  6919  iinpreima  7008  ftpg  7095  fsnunf  7125  f1prex  7224  soisores  7267  isotr  7276  off  7634  coof  7640  caofrss  7655  caonncan  7660  fvmpocurryd  8207  oaf1o  8484  omeulem1  8503  oeordi  8508  oelimcl  8521  oeeulem  8522  oeeui  8523  oaabs2  8570  omabs  8572  coflton  8592  pmresg  8800  ralxpmap  8826  domunsncan  8997  sucdom2  9119  unxpdom2  9151  sucxpdom  9152  unblem4  9186  fodomfi  9203  fodomfiOLD  9221  hartogslem1  9435  cantnflt  9569  cantnflem3  9588  cantnflem4  9589  cnfcomlem  9596  cnfcom  9597  ttrcltr  9613  infxpenlem  9911  infxpenc  9916  fseqenlem1  9922  pwsdompw  10101  cfeq0  10154  cofsmo  10167  cfsmolem  10168  ssfin4  10208  hsmexlem4  10327  hsmexlem5  10328  axdc3lem2  10349  fpwwe2  10541  wunpr  10607  mulclpi  10791  mulcanenq  10858  distrlem4pr  10924  prlem934  10931  prlem936  10945  divge0d  12976  elfzodif0  13672  elfznelfzob  13676  seqcaopr2  13947  facavg  14210  swrdwrdsymb  14572  cats1un  14630  f1oun2prg  14826  sqrtdiv  15174  sqrtdivd  15333  mulcn2  15505  o1of2  15522  fsumsplit  15650  sumsplit  15677  isumless  15754  demoivreALT  16112  rpnnen2lem11  16135  gcdnncl  16420  qredeu  16571  rpdvds  16573  isprm5  16620  rpexp  16635  prmdvdsbc  16639  divnumden  16661  divdenle  16662  phimullem  16692  phisum  16704  pythagtriplem4  16733  pythagtriplem8  16737  pythagtriplem9  16738  pcgcd1  16791  sumhash  16810  fldivp1  16811  pockthlem  16819  setsfun  17084  setsfun0  17085  ssc2  17731  estrreslem1  18045  tleile  18327  chnind  18529  sgrppropd  18641  mndpropd  18669  grpidssd  18931  grpinvssd  18932  issubg2  19056  isnsg3  19074  eqgid  19094  kerf1ghm  19161  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmqusker  19201  gass  19215  symgextres  19339  gsmsymgreqlem2  19345  sylow1lem5  19516  sylow2alem2  19532  sylow3lem3  19543  efgredlemd  19658  efgredlem  19661  frgpnabllem1  19787  frgpnabllem2  19788  subgdmdprd  19950  ablfacrplem  19981  omndmul3  20048  gsumle  20059  rglcom4d  20131  issrngd  20772  orngmul  20782  lmodprop2d  20859  lsspropd  20953  pwssplit1  20995  lspvadd  21032  rhmpreimaidl  21216  znidomb  21500  znrrg  21504  lindfind  21755  lindsind  21756  mplsubglem  21937  mplind  22006  ressply1evl  22286  mat1ghm  22399  mdetunilem1  22528  mdetunilem3  22530  mdetunilem4  22531  mdetunilem9  22536  cramerimplem2  22600  mat2pmatlin  22651  monmatcollpw  22695  cpmadugsumlemF  22792  mretopd  23008  neiptopnei  23048  neitr  23096  ufilen  23846  flimrest  23899  flimclslem  23900  fclsrest  23940  cnextcn  23983  haustsms2  24053  tsmsxplem2  24070  trust  24145  utoptop  24150  restutop  24153  ustuqtop4  24160  utopsnneiplem  24163  utop2nei  24166  utop3cls  24167  isucn2  24194  ucncn  24200  fmucnd  24207  trcfilu  24209  comet  24429  metustexhalf  24472  metustbl  24482  psmetutop  24483  nrmmetd  24490  reconnlem1  24743  reconnlem2  24744  fsumcn  24789  cmetcaulem  25216  iscmet3lem1  25219  iscmet3lem2  25220  bcthlem5  25256  cmslsschl  25305  rrxdstprj1  25337  minveclem4  25360  ovolfiniun  25430  itg1addlem4  25628  itg1addlem5  25629  itgsplitioo  25767  c1liplem1  25929  dvfsumlem1  25960  plyeq0lem  26143  quotcan  26245  psercnlem1  26363  cxplea  26633  birthdaylem3  26891  musumsum  27130  mpodvdsmulf1o  27132  dvdsmulf1o  27134  dchrelbas4  27182  dchrhash  27210  gausslemma2dlem0d  27298  gausslemma2dlem1a  27304  2lgslem1a1  27328  2sqlem8a  27364  2sqlem8  27365  2sqcoprm  27374  2sqmod  27375  chto1ub  27415  vmadivsum  27421  dchrisumlem1  27428  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  rpvmasum2  27451  mulog2sumlem2  27474  selberg2lem  27489  pntrmax  27503  pntpbnd1  27525  pntlemb  27536  pntlemj  27542  noextend  27606  cuteq0  27777  tgjustc1  28454  tgjustc2  28455  ercgrg  28496  motcgr  28515  tglineeltr  28610  colline  28628  miriso  28649  midexlem  28671  perpneq  28693  foot  28701  f1otrg  28850  axcontlem9  28952  uspgr1ewop  29228  nbupgrres  29344  structtocusgr  29426  wlkp1  29660  clwlkl1loop  29763  uspgrn2crct  29788  crctcshwlkn0lem5  29794  3trlond  30155  3pthond  30157  3spthond  30159  frgr3v  30257  vdgn1frgrv2  30278  numclwwlk3  30367  nmblolbii  30781  minvecolem3  30858  minvecolem4  30862  htthlem  30899  bcs2  31164  nmopub2tALT  31891  nmfnleub2  31908  eighmorth  31946  nmophmi  32013  nmopcoadji  32083  hstle  32212  atcvat3i  32378  opreu2reuALT  32458  prssad  32511  prssbd  32512  iinabrex  32551  disjxpin  32570  fmptco1f1o  32617  off2  32625  xppreima2  32635  fgreu  32656  suppovss  32666  1stpreimas  32691  padct  32705  resf1o  32717  fpwrelmap  32720  arginv  32735  argcj  32736  xrofsup  32754  eliccelico  32764  elicoelioo  32765  iocinif  32768  difioo  32769  suppssnn0  32792  hashpss  32796  elq2  32799  sgnsub  32825  2exple2exp  32833  oexpled  32835  indsupp  32855  indfsid  32857  ccatf1  32937  pfxlsw2ccat  32938  wrdt2ind  32941  ressprs  32954  xrge0addgt0  33005  xrge0adddir  33006  mndlactf1o  33018  mndractf1o  33019  gsumhashmul  33048  symgcom  33059  pmtrcnel  33065  pmtrcnel2  33066  pmtrcnelor  33067  cycpmfv2  33090  trsp2cyc  33099  cycpmco2lem7  33108  cyc3genpm  33128  cycpmconjslem2  33131  cyc3conja  33133  archirng  33164  archirngz  33165  rlocf1  33247  rrgsubm  33257  fracerl  33279  idomsubr  33282  linds2eq  33353  nsgqusf1olem3  33387  lidlunitel  33395  unitpidl1  33396  elrspunidl  33400  drngidl  33405  isprmidlc  33419  qsidomlem1  33424  qsidomlem2  33425  qsnzr  33427  mxidlirredi  33443  mxidlirred  33444  qsdrngi  33467  qsdrnglem2  33468  rprmasso  33497  1arithidomlem2  33508  1arithufdlem4  33519  zringidom  33523  deg1le0eq0  33543  ply1unit  33545  ply1dg1rt  33550  ply1dg3rt0irred  33553  m1pmeq  33554  mplvrpmrhm  33595  esplympl  33607  esplysply  33611  esplyind  33613  ply1degltdimlem  33656  ply1degltdim  33657  lindsunlem  33658  lbsdiflsp0  33660  fedgmullem1  33663  fedgmullem2  33664  assalactf1o  33669  ply1annprmidl  33741  minplyirredlem  33744  irngnminplynz  33746  minplyelirng  33749  algextdeglem4  33754  constrconj  33779  constrsqrtcl  33813  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  cos9thpinconstrlem1  33823  1smat1  33838  madjusmdetlem2  33862  qtophaus  33870  locfinref  33875  zarclssn  33907  zar0ring  33912  zarmxt1  33914  rhmpreimacnlem  33918  rhmpreimacn  33919  metideq  33927  sqsscirc2  33943  tpr2rico  33946  fmcncfil  33965  lmxrge0  33986  lmdvg  33987  qqhval2lem  34015  qqhf  34020  qqhnm  34024  esumle  34092  gsumesum  34093  esumlef  34096  esumrnmpt2  34102  esumpcvgval  34112  esum2d  34127  ofcf  34137  ldsysgenld  34194  ldgenpisyslem1  34197  unelros  34205  difelros  34206  inelsros  34212  diffiunisros  34213  imambfm  34296  omssubadd  34334  inelcarsg  34345  carsgsigalem  34349  carsggect  34352  carsgclctunlem2  34353  oddpwdc  34388  eulerpartlems  34394  eulerpartlemb  34402  eulerpartlemt  34405  iwrdsplit  34421  sseqf  34426  sseqfres  34427  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemfrcn0  34564  plymulx0  34581  signsplypnf  34584  signsvtn0  34604  signstfvneq0  34606  signsvtp  34617  signsvtn  34618  fsum2dsub  34641  reprlt  34653  hashreprin  34654  reprgt  34655  reprpmtf1o  34660  chtvalz  34663  breprexplema  34664  breprexplemc  34666  breprexp  34667  circlemeth  34674  logdivsqrle  34684  hgt750lemb  34690  lpadlem3  34712  lpadleft  34717  bnj1536  34887  bnj1001  34992  bnj1280  35053  fineqvnttrclselem2  35163  satffunlem1  35472  satffunlem2  35473  elmrsubrn  35585  neibastop3  36427  finxpsuclem  37462  poimirlem16  37696  poimirlem19  37699  poimirlem20  37700  poimirlem29  37709  mblfinlem3  37719  itg2addnclem3  37733  ftc1cnnclem  37751  lautlt  40210  lautcvr  40211  lauteq  40214  lautco  40216  ltrncl  40244  ltrncnvleN  40249  trljat2  40286  cdlemc6  40315  cdleme20c  40430  cdleme20j  40437  cdleme22e  40463  cdleme22eALTN  40464  cdlemg7aN  40744  cdlemg12e  40766  cdlemg17dALTN  40783  cdlemh  40936  cdlemkfid1N  41040  dibglbN  41285  diblss  41289  diclspsn  41313  dih1  41405  dihglbcpreN  41419  dihmeetlem4preN  41425  lcfrlem19  41680  aks4d1p8d1  42197  evlsvvval  42681  fsuppind  42708  mapfzcons  42833  mzpcl34  42848  mzpindd  42863  mzpsubst  42865  diophrw  42876  diophren  42930  irrapxlem1  42939  pellexlem5  42950  acongrep  43097  pwssplit4  43206  omlimcl2  43359  onexoegt  43361  oasubex  43403  omlim2  43416  nnoeomeqom  43429  nnawordexg  43444  succlg  43445  oacl2g  43447  onmcl  43448  omabs2  43449  omcl2  43450  tfsconcatrev  43465  ofoafg  43471  ofoaf  43472  ofoaass  43477  naddcnfass  43486  naddwordnexlem4  43518  omssrncard  43657  brtrclfv2  43844  rfovcnvf1od  44121  ntrk0kbimka  44156  isotone1  44165  isotone2  44166  4an4132  44616  modelaxrep  45098  mulltgt0  45143  fnchoice  45150  3adantlr3  45161  3adantll2  45162  3adantll3  45163  uzwo4  45174  disjf1o  45312  supxrgelem  45460  infleinflem2  45493  xrralrecnnle  45505  supxrunb3  45521  unb2ltle  45537  infrpgernmpt  45587  iooiinicc  45666  iooiinioc  45680  fmuldfeq  45707  mccl  45722  limccog  45744  limcrecl  45753  lptioo1  45756  islpcn  45761  limsupre  45763  neglimc  45769  0ellimcdiv  45771  limclner  45773  climleltrp  45798  climinf3  45838  liminflimsupclim  45929  xlimpnfxnegmnf  45936  icccncfext  46009  fprodcncf  46022  dvnmptdivc  46060  dvnmul  46065  dvmptfprod  46067  dvnprodlem3  46070  stoweidlem25  46147  stoweidlem34  46156  stoweidlem38  46160  stoweidlem44  46166  stoweidlem48  46170  stoweidlem49  46171  stoweidlem59  46181  stoweidlem60  46182  wallispilem4  46190  stirlinglem5  46200  dirkercncflem2  46226  fourierdlem39  46268  fourierdlem42  46271  fourierdlem46  46274  fourierdlem47  46275  fourierdlem48  46276  fourierdlem50  46278  fourierdlem51  46279  fourierdlem64  46292  fourierdlem73  46301  fourierdlem74  46302  fourierdlem77  46305  fourierdlem80  46308  fourierdlem87  46315  fourierdlem94  46322  fourierdlem103  46331  fourierdlem104  46332  etransclem32  46388  rrxsnicc  46422  sge0cl  46503  sge0f1o  46504  nnfoctbdjlem  46577  ismeannd  46589  omeiunltfirp  46641  hoicvr  46670  ovncvrrp  46686  hoidmvlelem2  46718  hoidmvlelem5  46721  hspdifhsp  46738  hoiqssbllem2  46745  hspmbllem2  46749  vonicclem2  46806  smflimsuplem7  46948  fundcmpsurbijinj  47534  sqrtpwpw2p  47662  lincresunit2  48603  nnpw2pmod  48708  dignn0flhalflem1  48740  dignn0flhalf  48743  rrx2linest  48867  itsclc0yqsol  48889  itsclc0b  48897  brab2dd  48952  oppcendc  49143  imaidfu  49235  imasubc  49276  oppcthinendcALT  49566  functhinclem1  49569  functhinclem2  49570  fullthinc2  49576