Theorem sylan9eqr 2786

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 2784	. 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 2701

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

This theorem is referenced by:  sbcied2  3789  csbied2  3890  opthhausdorff0  5465  fun2ssres  6531  fcoi1  6702  fcoi2  6703  funssfv  6847  fvtp1  7135  nvof1o  7221  onuninsuci  7780  ot1stg  7945  ot2ndg  7946  el2xptp0  7978  mpomptsx  8006  dmmpossx  8008  fmpox  8009  2ndconst  8041  offsplitfpar  8059  mpoxopoveq  8159  rdgeq12  8342  rdgsucmptnf  8358  frsucmptn  8368  oev2  8448  oesuclem  8450  oawordeulem  8479  om00  8500  omass  8505  omeulem1  8507  oeoa  8522  oeoe  8524  nnmass  8549  oaabs2  8574  omabs  8576  mapsnend  8968  omxpenlem  9002  sbthlem4  9014  sbthlem6  9016  fodomr  9052  ssenen  9075  fodomfir  9237  fi0  9329  cantnfp1  9596  cnfcomlem  9614  ttrclselem2  9641  cardaleph  10002  cflim2  10176  axdc4lem  10368  fpwwe2lem11  10554  fpwwe2lem12  10555  rankcf  10690  inatsk  10691  ltrnq  10892  addclprlem1  10929  mulclprlem  10932  1idpr  10942  prlem936  10960  reclem3pr  10962  mulcmpblnrlem  10983  recexsrlem  11016  map2psrpr  11023  addid0  11557  subdivcomb2  11838  nnnn0addcl  12432  zindd  12595  qaddcl  12884  qmulcl  12886  qreccl  12888  xaddnemnf  13156  xaddnepnf  13157  xaddcom  13160  xnegdi  13168  xaddass  13169  xpncan  13171  xleadd1a  13173  xlt2add  13180  rexmul  13191  xmulgt0  13203  xmulge0  13204  xmulasslem3  13206  xlemul1a  13208  xadddilem  13214  xadddi2  13217  modmuladd  13838  modm1p1mod0  13847  modfzo0difsn  13868  seqf1olem2  13967  expp1  13993  expneg  13994  expcllem  13997  mulexp  14026  expmul  14032  sqoddm1div8  14168  bcpasc  14246  hashrabsn01  14298  fseq1hash  14301  hashinfxadd  14310  hashfzo  14354  fnfz0hash  14371  ffzo0hash  14374  hashf1lem1  14380  hashge2el2dif  14405  hash3tpexb  14419  hashdifsnp1  14431  lsw0  14490  ccatval1  14502  ccatval2  14503  swrdval  14568  ccatopth  14640  reuccatpfxs1  14671  splval  14675  repswswrd  14708  2cshwcshw  14750  s4dom  14844  wrdlen2i  14867  shftfn  14998  reim0b  15044  cjexp  15075  sqeqd  15091  fsumser  15655  sumsnf  15668  binomlem  15754  expcnv  15789  prodsn  15887  prodsnf  15889  bpolylem  15973  bpoly2  15982  bpoly3  15983  ef0lem  16003  dvdsnegb  16202  mod2eq1n2dvds  16276  m1expe  16303  m1expo  16304  m1exp1  16305  flodddiv4  16344  sadadd2lem2  16379  bezoutr1  16498  dvdslcm  16527  lcmeq0  16529  lcmcl  16530  lcmabs  16534  lcmgcdlem  16535  lcmdvds  16537  lcmf0val  16551  lcmftp  16565  lcmfunsnlem2  16569  mulgcddvds  16584  divgcdcoprmex  16595  pcge0  16792  pcadd  16819  pcmpt2  16823  prmreclem4  16849  ramval  16938  ramcl  16959  fvprmselelfz  16974  fvprmselgcd1  16975  ressid2  17163  ressval2  17164  mndind  18720  frmdval  18743  efmnd  18762  smndex1igid  18796  smndex1n0mnd  18804  mgm2nsgrplem3  18812  mulgfval  18966  mulgfvalALT  18967  mulgnn0subcl  18984  mulgnn0z  18998  cycsubm  19099  f1ghm0to0  19142  isga  19188  symgextfve  19316  symgfixf1  19334  f1omvdco2  19345  psgnsn  19417  odid  19435  gexid  19478  efgsval2  19630  frgpuptinv  19668  frgpup2  19673  dprdsn  19935  srgmulgass  20120  srgpcomp  20121  srgbinomlem4  20132  ringinvnzdiv  20204  rngcval  20521  ringcval  20550  isabvd  20715  issrng  20747  lmodvsmmulgdi  20818  mptscmfsupp0  20848  lvecinv  21038  lspdisj2  21052  lspfixed  21053  lspexch  21054  sralem  21098  srasca  21102  sravsca  21103  sraip  21104  znval  21460  psgndiflemB  21525  isphl  21553  assamulgscmlem2  21825  mplval  21914  opsrval  21969  psdmvr  22072  cply1mul  22199  gsummoncoe1  22211  evl1fval  22231  scmate  22413  scmatscm  22416  mdetdiagid  22503  mdetunilem7  22521  mdetuni0  22524  gsummatr01lem3  22560  gsummatr01lem4  22561  gsummatr01  22562  slesolinvbi  22584  cpmatacl  22619  cpmatinvcl  22620  pmatcollpw2lem  22680  monmatcollpw  22682  pmatcollpwfi  22685  mp2pm2mplem4  22712  pm2mp  22728  cpmadugsumlemF  22779  cpmadugsumfi  22780  cpmadumatpoly  22786  cayhamlem4  22791  cayleyhamilton0  22792  cayleyhamiltonALT  22794  indistopon  22904  0ntr  22974  pnrmopn  23246  reftr  23417  kgenval  23438  pt1hmeo  23709  fmval  23846  fmf  23848  istmd  23977  istgp  23980  tsmsval2  24033  isxmet2d  24231  xpsxmetlem  24283  xpsmet  24286  blfvalps  24287  tmsval  24385  isnlm  24579  nmoleub  24635  idnghm  24647  blssioo  24699  blcvx  24702  icccvx  24864  pcorevlem  24942  isclm  24980  caufval  25191  iscms  25261  mbfsup  25581  i1f1  25607  dvexp3  25898  rolle  25910  dvivth  25931  deg1add  26024  0dgr  26166  coefv0  26169  elqaalem2  26244  dvradcnv  26346  abelthlem8  26365  efper  26404  logtayl  26585  abscxpbnd  26679  relogbcxpb  26713  logbgcd1irr  26720  dcubic2  26770  rlimcnp2  26892  cvxcl  26911  zetacvg  26941  lgamgulmlem2  26956  vmaval  27039  chtub  27139  logexprlim  27152  dchrsum2  27195  sumdchr2  27197  bposlem2  27212  lgsdir  27259  lgsne0  27262  lgsdirnn0  27271  lgsdinn0  27272  lgsquadlem2  27308  2lgslem3a  27323  2lgslem3b  27324  2lgslem3c  27325  2lgslem3d  27326  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  2sqn0  27361  dchrvmasum2if  27424  dchrvmasumiflem1  27428  rpvmasum2  27439  pntpbnd1  27513  ostth2lem4  27563  expsp1  28339  trgcgrg  28478  tgcgr4  28494  ax5seglem1  28891  ax5seglem2  28892  ax5seglem5  28896  usgr1vr  29218  cplgr2vpr  29396  cplgr3v  29398  cusgrrusgr  29545  wlklenvm1  29585  wlk0prc  29616  wlksoneq1eq2  29626  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem6  29778  crctcshlem4  29783  crctcsh  29787  wlkiswwlks1  29830  wwlksnext  29856  wwlksnextbi  29857  wwlksnextwrd  29860  midwwlks2s3  29915  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2a4  29959  clwlkclwwlklem3  29963  clwwisshclwws  29977  erclwwlkeqlen  29981  clwwlkinwwlk  30002  clwwlkn2  30006  clwwlkf  30009  clwwlkf1  30011  eleclclwwlknlem2  30023  erclwwlkneqlen  30030  umgrhashecclwwlk  30040  eucrctshift  30205  eucrct2eupth  30207  fusgr2wsp2nb  30296  grpoidinvlem2  30467  vcz  30537  nvz  30631  lnon0  30760  ipasslem2  30794  htthlem  30879  hvpncan  31001  hiidge0  31060  normgt0  31089  hsn0elch  31210  shsel3  31277  spansneleq  31532  normcan  31538  h1datomi  31543  fh1  31580  spansncvi  31614  5oalem1  31616  5oalem3  31618  5oalem5  31620  3oalem2  31625  pjdsi  31674  kbpj  31918  0hmop  31945  0lnfn  31947  adj0  31956  nlelshi  32022  branmfn  32067  opsqrlem1  32102  hst1h  32189  mdsl0  32272  superpos  32316  sumdmdlem  32380  cdj3lem1  32396  f1od2  32677  xrpxdivcld  32888  xrge0npcan  32987  elrgspnlem2  33196  rlocf1  33226  resvid2  33281  resvval2  33282  qsdrng  33447  r1pquslmic  33555  rtelextdg2lem  33695  esumsnf  34033  esummulc1  34050  measxun2  34179  omsmeas  34293  sibfof  34310  probun  34389  signstfvn  34539  bnj517  34854  pthhashvtx  35103  ex-sategoelel  35396  mrsubfval  35483  msrval  35513  dfrdg2  35771  itgeq12i  36182  bj-prmoore  37091  bj-bary1lem1  37287  rdgeqoa  37346  finxpreclem2  37366  finxpreclem3  37369  matunitlindflem1  37598  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem14  37616  poimirlem15  37617  poimirlem17  37619  poimirlem20  37622  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  mblfinlem2  37640  mblfinlem3  37641  ismblfin  37643  mbfposadd  37649  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  ftc1anclem8  37682  areacirc  37695  ismtyval  37782  ismrer1  37820  grposnOLD  37864  rabeq12f  38139  csbeq12  38140  iuneq12f  38145  lsatcv1  39029  glbconN  39358  glbconNOLD  39359  atltcvr  39417  3dim2  39450  islln2a  39499  2at0mat0  39507  islpln2a  39530  islvol2aN  39574  pmodlem2  39829  pmapjat1  39835  pcl0bN  39905  osumclN  39949  pexmidALTN  39960  lhp2at0nle  40017  4atexlemunv  40048  cdleme18b  40274  cdleme31sn1  40363  cdleme31sde  40367  cdleme31sn2  40371  ltrniotavalbN  40566  trljco  40722  cdlemh  40799  cdlemk40t  40900  cdlemk40f  40901  cdleml9  40966  dihmeetlem3N  41287  dochkrshp  41368  dihprrn  41408  dihjat1  41411  dvh3dim  41428  dochkrsm  41440  dochexmid  41450  lcfl7lem  41481  lcfl9a  41487  lclkrlem1  41488  mapdspex  41650  mapdindp2  41703  mapdh6dN  41721  hdmap1l6d  41795  hdmap11lem2  41824  hdmap14lem4a  41853  hdmapip0  41897  hlhilset  41916  nnadd1com  42243  mulgt0b2d  42454  fiabv  42512  prjspner1  42602  0prjspnrel  42603  jm2.26a  42976  onov0suclim  43250  oe0suclim  43253  cantnfresb  43300  onmcl  43307  omcl2  43309  tfsconcatun  43313  naddwordnexlem4  43377  mnringmulrcld  44204  radcnvrat  44290  sumsnd  45007  icccncfext  45872  fperdvper  45904  dvcosax  45911  ioodvbdlimc1lem1  45916  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  volioc  45957  itgiccshift  45965  stoweidlem34  46019  dirkercncflem2  46089  fourierdlem32  46124  fourierdlem41  46133  fourierdlem48  46139  fourierdlem64  46155  fourierdlem73  46164  fourierdlem79  46170  fourierdlem82  46173  fourierdlem97  46188  fourierdlem101  46192  fourierdlem109  46200  fourierdlem111  46202  fouriersw  46216  elaa2  46219  etransclem24  46243  etransclem25  46244  etransclem46  46265  nnfoctbdjlem  46440  ismeannd  46452  smfpimltxr  46732  smfpimgtxr  46765  ndfatafv2undef  47200  fzopredsuc  47311  m1modmmod  47346  modlt0b  47351  prproropf1olem3  47493  prproropf1olem4  47494  fmtnorec2lem  47530  2pwp1prmfmtno  47578  sfprmdvdsmersenne  47591  sgprmdvdsmersenne  47592  lighneallem2  47594  lighneallem3  47595  dfodd6  47625  dfeven4  47626  m1expevenALTV  47635  isubgredg  47854  upgrimwlklem5  47889  gricushgr  47905  stgrusgra  47947  isubgr3stgrlem8  47961  clintopval  48192  lmod0rng  48217  zlidlring  48222  2zrngagrp  48237  dmmpossx2  48325  zlmodzxzscm  48345  zlmodzxzadd  48346  domnmsuppn0  48357  rmsuppss  48358  scmsuppss  48359  ply1mulgsumlem4  48378  ldepsprlem  48461  lincresunit2  48467  nn0sumshdiglemB  48609  2arymptfv  48639  ackval42  48685  affinecomb1  48691  itschlc0yqe  48749  itsclquadb  48765  2itscp  48770  incat  49590  0setrec  49693