Theorem sylan9eqr 2787

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)

Hypotheses

Ref	Expression
sylan9eqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
sylan9eqr.2	⊢ (𝜓 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sylan9eqr	⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Proof of Theorem sylan9eqr

Step	Hyp	Ref	Expression
1		sylan9eqr.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sylan9eqr.2	. . 3 ⊢ (𝜓 → 𝐵 = 𝐶)
3	1, 2	sylan9eq 2785	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 458	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  sbcied2  3800  csbied2  3901  opthhausdorff0  5480  fun2ssres  6563  fcoi1  6736  fcoi2  6737  funssfv  6881  fvtp1  7171  nvof1o  7257  onuninsuci  7818  ot1stg  7984  ot2ndg  7985  el2xptp0  8017  mpomptsx  8045  dmmpossx  8047  fmpox  8048  2ndconst  8082  offsplitfpar  8100  mpoxopoveq  8200  rdgeq12  8383  rdgsucmptnf  8399  frsucmptn  8409  oev2  8489  oesuclem  8491  oawordeulem  8520  om00  8541  omass  8546  omeulem1  8548  oeoa  8563  oeoe  8565  nnmass  8590  oaabs2  8615  omabs  8617  mapsnend  9009  omxpenlem  9046  sbthlem4  9059  sbthlem6  9061  fodomr  9097  ssenen  9120  fodomfir  9285  fi0  9377  cantnfp1  9640  cnfcomlem  9658  ttrclselem2  9685  cardaleph  10048  cflim2  10222  axdc4lem  10414  fpwwe2lem11  10600  fpwwe2lem12  10601  rankcf  10736  inatsk  10737  ltrnq  10938  addclprlem1  10975  mulclprlem  10978  1idpr  10988  prlem936  11006  reclem3pr  11008  mulcmpblnrlem  11029  recexsrlem  11062  map2psrpr  11069  addid0  11603  subdivcomb2  11884  nnnn0addcl  12478  zindd  12641  qaddcl  12930  qmulcl  12932  qreccl  12934  xaddnemnf  13202  xaddnepnf  13203  xaddcom  13206  xnegdi  13214  xaddass  13215  xpncan  13217  xleadd1a  13219  xlt2add  13226  rexmul  13237  xmulgt0  13249  xmulge0  13250  xmulasslem3  13252  xlemul1a  13254  xadddilem  13260  xadddi2  13263  modmuladd  13884  modm1p1mod0  13893  modfzo0difsn  13914  seqf1olem2  14013  expp1  14039  expneg  14040  expcllem  14043  mulexp  14072  expmul  14078  sqoddm1div8  14214  bcpasc  14292  hashrabsn01  14344  fseq1hash  14347  hashinfxadd  14356  hashfzo  14400  fnfz0hash  14417  ffzo0hash  14420  hashf1lem1  14426  hashge2el2dif  14451  hash3tpexb  14465  hashdifsnp1  14477  lsw0  14536  ccatval1  14548  ccatval2  14549  swrdval  14614  ccatopth  14687  reuccatpfxs1  14718  splval  14722  repswswrd  14755  2cshwcshw  14797  s4dom  14891  wrdlen2i  14914  shftfn  15045  reim0b  15091  cjexp  15122  sqeqd  15138  fsumser  15702  sumsnf  15715  binomlem  15801  expcnv  15836  prodsn  15934  prodsnf  15936  bpolylem  16020  bpoly2  16029  bpoly3  16030  ef0lem  16050  dvdsnegb  16249  mod2eq1n2dvds  16323  m1expe  16350  m1expo  16351  m1exp1  16352  flodddiv4  16391  sadadd2lem2  16426  bezoutr1  16545  dvdslcm  16574  lcmeq0  16576  lcmcl  16577  lcmabs  16581  lcmgcdlem  16582  lcmdvds  16584  lcmf0val  16598  lcmftp  16612  lcmfunsnlem2  16616  mulgcddvds  16631  divgcdcoprmex  16642  pcge0  16839  pcadd  16866  pcmpt2  16870  prmreclem4  16896  ramval  16985  ramcl  17006  fvprmselelfz  17021  fvprmselgcd1  17022  ressid2  17210  ressval2  17211  mndind  18761  frmdval  18784  efmnd  18803  smndex1igid  18837  smndex1n0mnd  18845  mgm2nsgrplem3  18853  mulgfval  19007  mulgfvalALT  19008  mulgnn0subcl  19025  mulgnn0z  19039  cycsubm  19140  f1ghm0to0  19183  isga  19229  symgextfve  19355  symgfixf1  19373  f1omvdco2  19384  psgnsn  19456  odid  19474  gexid  19517  efgsval2  19669  frgpuptinv  19707  frgpup2  19712  dprdsn  19974  srgmulgass  20132  srgpcomp  20133  srgbinomlem4  20144  ringinvnzdiv  20216  rngcval  20533  ringcval  20562  isabvd  20727  issrng  20759  lmodvsmmulgdi  20809  mptscmfsupp0  20839  lvecinv  21029  lspdisj2  21043  lspfixed  21044  lspexch  21045  sralem  21089  srasca  21093  sravsca  21094  sraip  21095  znval  21451  psgndiflemB  21515  isphl  21543  assamulgscmlem2  21815  mplval  21904  opsrval  21959  psdmvr  22062  cply1mul  22189  gsummoncoe1  22201  evl1fval  22221  scmate  22403  scmatscm  22406  mdetdiagid  22493  mdetunilem7  22511  mdetuni0  22514  gsummatr01lem3  22550  gsummatr01lem4  22551  gsummatr01  22552  slesolinvbi  22574  cpmatacl  22609  cpmatinvcl  22610  pmatcollpw2lem  22670  monmatcollpw  22672  pmatcollpwfi  22675  mp2pm2mplem4  22702  pm2mp  22718  cpmadugsumlemF  22769  cpmadugsumfi  22770  cpmadumatpoly  22776  cayhamlem4  22781  cayleyhamilton0  22782  cayleyhamiltonALT  22784  indistopon  22894  0ntr  22964  pnrmopn  23236  reftr  23407  kgenval  23428  pt1hmeo  23699  fmval  23836  fmf  23838  istmd  23967  istgp  23970  tsmsval2  24023  isxmet2d  24221  xpsxmetlem  24273  xpsmet  24276  blfvalps  24277  tmsval  24375  isnlm  24569  nmoleub  24625  idnghm  24637  blssioo  24689  blcvx  24692  icccvx  24854  pcorevlem  24932  isclm  24970  caufval  25181  iscms  25251  mbfsup  25571  i1f1  25597  dvexp3  25888  rolle  25900  dvivth  25921  deg1add  26014  0dgr  26156  coefv0  26159  elqaalem2  26234  dvradcnv  26336  abelthlem8  26355  efper  26394  logtayl  26575  abscxpbnd  26669  relogbcxpb  26703  logbgcd1irr  26710  dcubic2  26760  rlimcnp2  26882  cvxcl  26901  zetacvg  26931  lgamgulmlem2  26946  vmaval  27029  chtub  27129  logexprlim  27142  dchrsum2  27185  sumdchr2  27187  bposlem2  27202  lgsdir  27249  lgsne0  27252  lgsdirnn0  27261  lgsdinn0  27262  lgsquadlem2  27298  2lgslem3a  27313  2lgslem3b  27314  2lgslem3c  27315  2lgslem3d  27316  2lgslem3a1  27317  2lgslem3b1  27318  2lgslem3c1  27319  2lgslem3d1  27320  2sqn0  27351  dchrvmasum2if  27414  dchrvmasumiflem1  27418  rpvmasum2  27429  pntpbnd1  27503  ostth2lem4  27553  expsp1  28321  trgcgrg  28448  tgcgr4  28464  ax5seglem1  28861  ax5seglem2  28862  ax5seglem5  28866  usgr1vr  29188  cplgr2vpr  29366  cplgr3v  29368  cusgrrusgr  29515  wlklenvm1  29556  wlk0prc  29588  wlksoneq1eq2  29598  crctcshwlkn0lem4  29749  crctcshwlkn0lem5  29750  crctcshwlkn0lem6  29751  crctcshlem4  29756  crctcsh  29760  wlkiswwlks1  29803  wwlksnext  29829  wwlksnextbi  29830  wwlksnextwrd  29833  midwwlks2s3  29888  clwlkclwwlklem2fv1  29930  clwlkclwwlklem2a4  29932  clwlkclwwlklem3  29936  clwwisshclwws  29950  erclwwlkeqlen  29954  clwwlkinwwlk  29975  clwwlkn2  29979  clwwlkf  29982  clwwlkf1  29984  eleclclwwlknlem2  29996  erclwwlkneqlen  30003  umgrhashecclwwlk  30013  eucrctshift  30178  eucrct2eupth  30180  fusgr2wsp2nb  30269  grpoidinvlem2  30440  vcz  30510  nvz  30604  lnon0  30733  ipasslem2  30767  htthlem  30852  hvpncan  30974  hiidge0  31033  normgt0  31062  hsn0elch  31183  shsel3  31250  spansneleq  31505  normcan  31511  h1datomi  31516  fh1  31553  spansncvi  31587  5oalem1  31589  5oalem3  31591  5oalem5  31593  3oalem2  31598  pjdsi  31647  kbpj  31891  0hmop  31918  0lnfn  31920  adj0  31929  nlelshi  31995  branmfn  32040  opsqrlem1  32075  hst1h  32162  mdsl0  32245  superpos  32289  sumdmdlem  32353  cdj3lem1  32369  f1od2  32650  xrpxdivcld  32861  xrge0npcan  32967  elrgspnlem2  33200  rlocf1  33230  resvid2  33308  resvval2  33309  qsdrng  33474  r1pquslmic  33582  rtelextdg2lem  33722  esumsnf  34060  esummulc1  34077  measxun2  34206  omsmeas  34320  sibfof  34337  probun  34416  signstfvn  34566  bnj517  34881  pthhashvtx  35115  ex-sategoelel  35408  mrsubfval  35495  msrval  35525  dfrdg2  35778  itgeq12i  36189  bj-prmoore  37098  bj-bary1lem1  37294  rdgeqoa  37353  finxpreclem2  37373  finxpreclem3  37376  matunitlindflem1  37605  poimirlem1  37610  poimirlem2  37611  poimirlem3  37612  poimirlem4  37613  poimirlem5  37614  poimirlem6  37615  poimirlem7  37616  poimirlem10  37619  poimirlem11  37620  poimirlem12  37621  poimirlem14  37623  poimirlem15  37624  poimirlem17  37626  poimirlem20  37629  poimirlem22  37631  poimirlem23  37632  poimirlem24  37633  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  mblfinlem2  37647  mblfinlem3  37648  ismblfin  37650  mbfposadd  37656  itg2addnclem  37660  itg2addnclem3  37662  itg2addnc  37663  ftc1anclem8  37689  areacirc  37702  ismtyval  37789  ismrer1  37827  grposnOLD  37871  rabeq12f  38146  csbeq12  38147  iuneq12f  38152  lsatcv1  39036  glbconN  39365  glbconNOLD  39366  atltcvr  39424  3dim2  39457  islln2a  39506  2at0mat0  39514  islpln2a  39537  islvol2aN  39581  pmodlem2  39836  pmapjat1  39842  pcl0bN  39912  osumclN  39956  pexmidALTN  39967  lhp2at0nle  40024  4atexlemunv  40055  cdleme18b  40281  cdleme31sn1  40370  cdleme31sde  40374  cdleme31sn2  40378  ltrniotavalbN  40573  trljco  40729  cdlemh  40806  cdlemk40t  40907  cdlemk40f  40908  cdleml9  40973  dihmeetlem3N  41294  dochkrshp  41375  dihprrn  41415  dihjat1  41418  dvh3dim  41435  dochkrsm  41447  dochexmid  41457  lcfl7lem  41488  lcfl9a  41494  lclkrlem1  41495  mapdspex  41657  mapdindp2  41710  mapdh6dN  41728  hdmap1l6d  41802  hdmap11lem2  41831  hdmap14lem4a  41860  hdmapip0  41904  hlhilset  41923  nnadd1com  42250  mulgt0b2d  42461  fiabv  42517  prjspner1  42607  0prjspnrel  42608  jm2.26a  42982  onov0suclim  43256  oe0suclim  43259  cantnfresb  43306  onmcl  43313  omcl2  43315  tfsconcatun  43319  naddwordnexlem4  43383  mnringmulrcld  44210  radcnvrat  44296  sumsnd  45013  icccncfext  45878  fperdvper  45910  dvcosax  45917  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  volioc  45963  itgiccshift  45971  stoweidlem34  46025  dirkercncflem2  46095  fourierdlem32  46130  fourierdlem41  46139  fourierdlem48  46145  fourierdlem64  46161  fourierdlem73  46170  fourierdlem79  46176  fourierdlem82  46179  fourierdlem97  46194  fourierdlem101  46198  fourierdlem109  46206  fourierdlem111  46208  fouriersw  46222  elaa2  46225  etransclem24  46249  etransclem25  46250  etransclem46  46271  nnfoctbdjlem  46446  ismeannd  46458  smfpimltxr  46738  smfpimgtxr  46771  ndfatafv2undef  47203  fzopredsuc  47314  m1modmmod  47349  modlt0b  47354  prproropf1olem3  47496  prproropf1olem4  47497  fmtnorec2lem  47533  2pwp1prmfmtno  47581  sfprmdvdsmersenne  47594  sgprmdvdsmersenne  47595  lighneallem2  47597  lighneallem3  47598  dfodd6  47628  dfeven4  47629  m1expevenALTV  47638  isubgredg  47856  upgrimwlklem5  47891  gricushgr  47907  stgrusgra  47948  isubgr3stgrlem8  47962  clintopval  48182  lmod0rng  48207  zlidlring  48212  2zrngagrp  48227  dmmpossx2  48315  zlmodzxzscm  48335  zlmodzxzadd  48336  domnmsuppn0  48347  rmsuppss  48348  scmsuppss  48349  ply1mulgsumlem4  48368  ldepsprlem  48451  lincresunit2  48457  nn0sumshdiglemB  48599  2arymptfv  48629  ackval42  48675  affinecomb1  48681  itschlc0yqe  48739  itsclquadb  48755  2itscp  48760  incat  49580  0setrec  49683