Theorem syl21anc 848

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bibiad  850  syl1111anc  851  rspc2dv  3598  wereu2  5646  frpomin  6329  funtpg  6578  funcnvtp  6586  funcnvqp  6587  fnund  6638  fun2d  6730  fvun1  6960  iinpreima  7052  ftpg  7141  fsnunf  7171  f1prex  7270  soisores  7313  isotr  7322  off  7680  coof  7686  caofrss  7701  caonncan  7706  fvmpocurryd  8253  oaf1o  8534  omeulem1  8553  oeordi  8559  oelimcl  8572  oeeulem  8573  oeeui  8574  oaabs2  8621  omabs  8623  coflton  8643  pmresg  8854  ralxpmap  8880  domunsncan  9051  sucdom2  9173  unxpdom2  9206  sucxpdom  9207  unblem4  9241  fodomfi  9258  hartogslem1  9492  cantnflt  9629  cantnflem3  9648  cantnflem4  9649  cnfcomlem  9656  cnfcom  9657  ttrcltr  9673  infxpenlem  9971  infxpenc  9976  fseqenlem1  9982  pwsdompw  10161  cfeq0  10215  cofsmo  10228  cfsmolem  10229  ssfin4  10269  hsmexlem4  10388  hsmexlem5  10389  axdc3lem2  10410  fpwwe2  10603  wunpr  10669  mulclpi  10853  mulcanenq  10920  distrlem4pr  10986  prlem934  10993  prlem936  11007  divge0d  13079  elfzodif0  13778  elfznelfzob  13782  seqcaopr2  14053  facavg  14316  swrdwrdsymb  14678  cats1un  14736  f1oun2prg  14932  sgnsub  15121  sqrtdiv  15294  sqrtdivd  15453  mulcn2  15625  o1of2  15642  fsumsplit  15770  sumsplit  15797  isumless  15877  demoivreALT  16235  rpnnen2lem11  16258  gcdnncl  16543  qredeu  16694  rpdvds  16696  isprm5  16744  rpexp  16759  prmdvdsbc  16763  divnumden  16785  divdenle  16786  phimullem  16816  phisum  16828  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  pcgcd1  16915  sumhash  16934  fldivp1  16935  pockthlem  16943  setsfun  17209  setsfun0  17210  ssc2  17857  estrreslem1  18171  tleile  18453  chnind  18655  sgrppropd  18767  mndpropd  18795  grpidssd  19060  grpinvssd  19061  issubg2  19185  isnsg3  19203  eqgid  19223  kerf1ghm  19289  ghmqusnsglem1  19322  ghmquskerlem1  19325  ghmqusker  19329  gass  19343  symgextres  19467  gsmsymgreqlem2  19473  sylow1lem5  19644  sylow2alem2  19660  sylow3lem3  19671  efgredlemd  19786  efgredlem  19789  frgpnabllem1  19915  frgpnabllem2  19916  subgdmdprd  20078  ablfacrplem  20109  omndmul3  20176  gsumle  20187  rglcom4d  20263  issrngd  20906  orngmul  20916  lmodprop2d  20993  lsspropd  21086  pwssplit1  21128  lspvadd  21165  rhmpreimaidl  21349  znidomb  21615  znrrg  21619  lindfind  21870  lindsind  21871  mplsubglem  22052  mplind  22125  evlsvvval  22148  ressply1evl  22435  mat1ghm  22545  mdetunilem1  22674  mdetunilem3  22676  mdetunilem4  22677  mdetunilem9  22682  cramerimplem2  22746  mat2pmatlin  22797  monmatcollpw  22841  cpmadugsumlemF  22938  mretopd  23154  neiptopnei  23194  neitr  23242  ufilen  23992  flimrest  24045  flimclslem  24046  fclsrest  24086  cnextcn  24129  haustsms2  24199  tsmsxplem2  24216  trust  24291  utoptop  24296  restutop  24299  ustuqtop4  24306  utopsnneiplem  24309  utop2nei  24312  utop3cls  24313  isucn2  24340  ucncn  24346  fmucnd  24353  trcfilu  24355  comet  24575  metustexhalf  24618  metustbl  24628  psmetutop  24629  nrmmetd  24636  reconnlem1  24889  reconnlem2  24890  fsumcn  24934  cmetcaulem  25352  iscmet3lem1  25355  iscmet3lem2  25356  bcthlem5  25392  cmslsschl  25441  rrxdstprj1  25473  minveclem4  25496  ovolfiniun  25565  itg1addlem4  25763  itg1addlem5  25764  itgsplitioo  25902  c1liplem1  26060  dvfsumlem1  26090  plyeq0lem  26272  plyn0mulidp  26347  quotcan  26375  psercnlem1  26490  cxplea  26763  birthdaylem3  27020  musumsum  27258  mpodvdsmulf1o  27260  dvdsmulf1o  27262  dchrelbas4  27309  dchrhash  27337  gausslemma2dlem0d  27425  gausslemma2dlem1a  27431  2lgslem1a1  27455  2sqlem8a  27491  2sqlem8  27492  2sqcoprm  27501  2sqmod  27502  chto1ub  27542  vmadivsum  27548  dchrisumlem1  27555  dchrvmasumlem2  27564  dchrvmasumiflem1  27567  rpvmasum2  27578  mulog2sumlem2  27601  selberg2lem  27616  pntrmax  27630  pntpbnd1  27652  pntlemb  27663  pntlemj  27669  noextend  27732  cuteq0  27910  tgjustc1  28646  tgjustc2  28647  ercgrg  28688  motcgr  28707  tglineeltr  28802  colline  28821  miriso  28845  midexlem  28867  perpneq  28889  foot  28897  f1otrg  29073  axcontlem9  29175  uspgr1ewop  29451  nbupgrres  29567  structtocusgr  29649  wlkp1  29882  clwlkl1loop  29985  uspgrn2crct  30010  crctcshwlkn0lem5  30016  3trlond  30377  3pthond  30379  3spthond  30381  frgr3v  30479  vdgn1frgrv2  30500  numclwwlk3  30589  nmblolbii  31004  minvecolem3  31081  minvecolem4  31085  htthlem  31122  bcs2  31387  nmopub2tALT  32114  nmfnleub2  32131  eighmorth  32169  nmophmi  32236  nmopcoadji  32306  hstle  32435  atcvat3i  32601  opreu2reuALT  32678  prssad  32730  prssbd  32731  iinabrex  32771  disjxpin  32790  fmptco1f1o  32837  off2  32845  xppreima2  32855  fgreu  32875  suppovss  32885  1stpreimas  32910  padct  32922  resf1o  32934  fpwrelmap  32937  arginv  32951  argcj  32952  xrofsup  32971  eliccelico  32981  elicoelioo  32982  iocinif  32985  difioo  32986  suppssnn0  33009  hashpss  33013  elq2  33016  2exple2exp  33038  oexpled  33040  indsupp  33047  indfsid  33049  ccatf1  33129  pfxlsw2ccat  33130  wrdt2ind  33133  ressprs  33146  xrge0addgt0  33197  xrge0adddir  33198  mndlactf1o  33210  mndractf1o  33211  gsumhashmul  33249  gsummulsubdishift1  33250  symgcom  33265  pmtrcnel  33271  pmtrcnel2  33272  pmtrcnelor  33273  cycpmfv2  33296  trsp2cyc  33305  cycpmco2lem7  33314  cyc3genpm  33334  cycpmconjslem2  33337  cyc3conja  33339  archirng  33370  archirngz  33371  rlocf1  33457  rlocisunit  33459  rrgsubm  33470  fracerl  33495  idomsubr  33498  linds2eq  33569  nsgqusf1olem3  33603  lidlunitel  33611  unitpidl1  33612  elrspunidl  33616  drngidl  33621  isprmidlc  33635  qsidomlem1  33641  qsidomlem2  33642  qsnzr  33644  mxidlirredi  33661  mxidlirred  33662  qsdrngi  33685  qsdrnglem2  33686  dflring2  33691  rprmasso  33723  1arithidomlem2  33734  1arithufdlem4  33745  zringidom  33749  deg1le0eq0  33771  ply1unit  33773  ply1dg1rt  33778  ply1dg3rt0irred  33782  m1pmeq  33783  selvply1rhmlema  33817  selvply1rhmlem1  33819  evlextv  33841  mplvrpmrhm  33846  esplympl  33866  esplysply  33870  esplyind  33874  esplyindfv  33875  vietadeg1  33877  ply1degltdimlem  33921  ply1degltdim  33922  lindsunlem  33923  lbsdiflsp0  33925  fedgmullem1  33928  fedgmullem2  33929  assalactf1o  33934  ply1annprmidl  34006  minplyirredlem  34009  irngnminplynz  34011  minplyelirng  34014  algextdeglem4  34019  constrconj  34044  constrsqrtcl  34078  cos9thpiminplylem1  34081  cos9thpiminplylem2  34082  cos9thpinconstrlem1  34088  1smat1  34103  madjusmdetlem2  34127  qtophaus  34135  locfinref  34140  zarclssn  34172  zar0ring  34177  zarmxt1  34179  rhmpreimacnlem  34183  rhmpreimacn  34184  metideq  34192  sqsscirc2  34208  tpr2rico  34211  fmcncfil  34230  lmxrge0  34251  lmdvg  34252  qqhval2lem  34280  qqhf  34285  qqhnm  34289  esumle  34357  gsumesum  34358  esumlef  34361  esumrnmpt2  34367  esumpcvgval  34377  esum2d  34392  ofcf  34402  ldsysgenld  34459  ldgenpisyslem1  34462  unelros  34470  difelros  34471  inelsros  34477  diffiunisros  34478  imambfm  34561  omssubadd  34599  inelcarsg  34610  carsgsigalem  34614  carsggect  34617  carsgclctunlem2  34618  oddpwdc  34653  eulerpartlems  34659  eulerpartlemb  34667  eulerpartlemt  34670  iwrdsplit  34686  sseqf  34691  sseqfres  34692  ballotlemfc0  34792  ballotlemfcc  34793  ballotlemfrcn0  34829  signsplypnf  34846  signsvtn0  34866  signstfvneq0  34868  signsvtp  34879  signsvtn  34880  fsum2dsub  34903  reprlt  34915  hashreprin  34916  reprgt  34917  reprpmtf1o  34922  chtvalz  34925  breprexplema  34926  breprexplemc  34928  breprexp  34929  circlemeth  34936  logdivsqrle  34946  hgt750lemb  34952  lpadlem3  34977  lpadleft  34982  bnj1536  35151  bnj1001  35256  bnj1280  35317  fineqvnttrclselem2  35422  satffunlem1  35762  satffunlem2  35763  elmrsubrn  35875  neibastop3  36727  finxpsuclem  37896  poimirlem16  38140  poimirlem19  38143  poimirlem20  38144  poimirlem29  38153  mblfinlem3  38163  itg2addnclem3  38177  ftc1cnnclem  38195  lautlt  40720  lautcvr  40721  lauteq  40724  lautco  40726  ltrncl  40754  ltrncnvleN  40759  trljat2  40796  cdlemc6  40825  cdleme20c  40940  cdleme20j  40947  cdleme22e  40973  cdleme22eALTN  40974  cdlemg7aN  41254  cdlemg12e  41276  cdlemg17dALTN  41293  cdlemh  41446  cdlemkfid1N  41550  dibglbN  41795  diblss  41799  diclspsn  41823  dih1  41915  dihglbcpreN  41929  dihmeetlem4preN  41935  lcfrlem19  42190  aks4d1p8d1  42706  fsuppind  43177  mapfzcons  43302  mzpcl34  43317  mzpindd  43332  mzpsubst  43334  diophrw  43345  diophren  43395  irrapxlem1  43404  pellexlem5  43415  acongrep  43562  pwssplit4  43671  omlimcl2  43824  onexoegt  43826  oasubex  43868  omlim2  43881  nnoeomeqom  43894  nnawordexg  43909  succlg  43910  oacl2g  43912  onmcl  43913  omabs2  43914  omcl2  43915  tfsconcatrev  43930  ofoafg  43936  ofoaf  43937  ofoaass  43942  naddcnfass  43951  naddwordnexlem4  43983  omssrncard  44121  brtrclfv2  44308  rfovcnvf1od  44585  ntrk0kbimka  44620  isotone1  44629  isotone2  44630  4an4132  45080  modelaxrep  45562  mulltgt0  45607  fnchoice  45614  3adantlr3  45625  3adantll2  45626  3adantll3  45627  uzwo4  45638  disjf1o  45774  supxrgelem  45918  infleinflem2  45951  xrralrecnnle  45963  supxrunb3  45979  unb2ltle  45994  infrpgernmpt  46044  iooiinicc  46123  iooiinioc  46137  fmuldfeq  46164  mccl  46179  limccog  46201  limcrecl  46210  lptioo1  46213  islpcn  46218  limsupre  46220  neglimc  46226  0ellimcdiv  46228  limclner  46230  climleltrp  46255  climinf3  46295  liminflimsupclim  46386  xlimpnfxnegmnf  46393  icccncfext  46466  fprodcncf  46479  dvnmptdivc  46517  dvnmul  46522  dvmptfprod  46524  dvnprodlem3  46527  stoweidlem25  46604  stoweidlem34  46613  stoweidlem38  46617  stoweidlem44  46623  stoweidlem48  46627  stoweidlem49  46628  stoweidlem59  46638  stoweidlem60  46639  wallispilem4  46647  stirlinglem5  46657  dirkercncflem2  46683  fourierdlem39  46725  fourierdlem42  46728  fourierdlem46  46731  fourierdlem47  46732  fourierdlem48  46733  fourierdlem50  46735  fourierdlem51  46736  fourierdlem64  46749  fourierdlem73  46758  fourierdlem74  46759  fourierdlem77  46762  fourierdlem80  46765  fourierdlem87  46772  fourierdlem94  46779  fourierdlem103  46788  fourierdlem104  46789  etransclem32  46845  rrxsnicc  46879  sge0cl  46960  sge0f1o  46961  nnfoctbdjlem  47034  ismeannd  47046  omeiunltfirp  47098  ovncvrrp  47143  hoidmvlelem2  47175  hoidmvlelem5  47178  hspdifhsp  47195  hoiqssbllem2  47202  hspmbllem2  47206  vonicclem2  47263  smflimsuplem7  47405  fundcmpsurbijinj  48021  sqrtpwpw2p  48152  lincresunit2  49105  nnpw2pmod  49210  dignn0flhalflem1  49242  dignn0flhalf  49245  rrx2linest  49369  itsclc0yqsol  49391  itsclc0b  49399  brab2dd  49454  oppcendc  49644  imaidfu  49736  imasubc  49777  oppcthinendcALT  50067  functhinclem1  50070  functhinclem2  50071  fullthinc2  50077