Theorem sylan9eqr 2880

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 2878	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	3	ancoms 461	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  sbcied2  3817  csbied2  3922  opthhausdorff0  5410  fun2ssres  6401  fcoi1  6554  fcoi2  6555  funssfv  6693  fvtp1  6959  nvof1o  7039  onuninsuci  7557  ot1stg  7705  ot2ndg  7706  el2xptp0  7738  mpomptsx  7764  dmmpossx  7766  fmpox  7767  2ndconst  7798  offsplitfpar  7817  mpoxopoveq  7887  wfrlem10  7966  rdgeq12  8051  rdgsucmptnf  8067  frsucmptn  8076  oev2  8150  oesuclem  8152  oawordeulem  8182  om00  8203  omass  8208  omeulem1  8210  oeoa  8225  oeoe  8227  nnmass  8252  oaabs2  8274  omabs  8276  mapsnend  8590  omxpenlem  8620  sbthlem4  8632  sbthlem6  8634  fodomr  8670  ssenen  8693  fi0  8886  cantnfp1  9146  cnfcomlem  9164  cardaleph  9517  cflim2  9687  axdc4lem  9879  fpwwe2lem12  10065  fpwwe2lem13  10066  rankcf  10201  inatsk  10202  ltrnq  10403  addclprlem1  10440  mulclprlem  10443  1idpr  10453  prlem936  10471  reclem3pr  10473  mulcmpblnrlem  10494  recexsrlem  10527  map2psrpr  10534  addid0  11061  subdivcomb2  11338  nnnn0addcl  11930  zindd  12086  qaddcl  12367  qmulcl  12369  qreccl  12371  xaddnemnf  12632  xaddnepnf  12633  xaddcom  12636  xnegdi  12644  xaddass  12645  xpncan  12647  xleadd1a  12649  xlt2add  12656  rexmul  12667  xmulgt0  12679  xmulge0  12680  xmulasslem3  12682  xlemul1a  12684  xadddilem  12690  xadddi2  12693  modmuladd  13284  modm1p1mod0  13293  modfzo0difsn  13314  seqf1olem2  13413  expp1  13439  expneg  13440  expcllem  13443  mulexp  13471  expmul  13477  sqoddm1div8  13607  bcpasc  13684  hashrabsn01  13737  fseq1hash  13740  hashinfxadd  13749  hashfzo  13793  fnfz0hash  13807  ffzo0hash  13810  hashf1lem1  13816  hashge2el2dif  13841  hashdifsnp1  13857  lsw0  13919  ccatval1  13932  ccatval1OLD  13933  ccatval2  13934  swrdval  14007  ccatopth  14080  reuccatpfxs1  14111  splval  14115  repswswrd  14148  2cshwcshw  14189  s4dom  14283  wrdlen2i  14306  shftfn  14434  reim0b  14480  cjexp  14511  sqeqd  14527  fsumser  15089  sumsnf  15101  binomlem  15186  expcnv  15221  prodsn  15318  prodsnf  15320  bpolylem  15404  bpoly2  15413  bpoly3  15414  ef0lem  15434  dvdsnegb  15629  mod2eq1n2dvds  15698  m1expe  15727  m1expo  15728  m1exp1  15729  flodddiv4  15766  sadadd2lem2  15801  gcdabs  15879  bezoutr1  15915  dvdslcm  15944  lcmeq0  15946  lcmcl  15947  lcmabs  15951  lcmgcdlem  15952  lcmdvds  15954  lcmf0val  15968  lcmftp  15982  lcmfunsnlem2  15986  mulgcddvds  16001  divgcdcoprmex  16012  pcge0  16200  pcadd  16227  pcmpt2  16231  prmreclem4  16257  ramval  16346  ramcl  16367  fvprmselelfz  16382  fvprmselgcd1  16383  ressid2  16554  ressval2  16555  mndind  17994  frmdval  18018  efmnd  18037  smndex1igid  18071  smndex1n0mnd  18079  mgm2nsgrplem3  18087  mulgfval  18228  mulgfvalALT  18229  mulgnn0subcl  18243  mulgnn0z  18256  cycsubm  18347  isga  18423  symgextfve  18549  symgfixf1  18567  f1omvdco2  18578  psgnsn  18650  odid  18668  gexid  18708  efgsval2  18861  frgpuptinv  18899  frgpup2  18904  dprdsn  19160  srgmulgass  19283  srgpcomp  19284  srgbinomlem4  19295  ringinvnzdiv  19345  f1ghm0to0  19494  f1rhm0to0OLD  19495  f1rhm0to0ALT  19496  isabvd  19593  issrng  19623  lmodvsmmulgdi  19671  mptscmfsupp0  19701  lvecinv  19887  lspdisj2  19901  lspfixed  19902  lspexch  19903  sralem  19951  srasca  19955  sravsca  19956  sraip  19957  assamulgscmlem2  20131  mplval  20210  opsrval  20257  cply1mul  20464  gsummoncoe1  20474  evl1fval  20493  znval  20684  psgndiflemB  20746  isphl  20774  scmate  21121  scmatscm  21124  mdetdiagid  21211  mdetunilem7  21229  mdetuni0  21232  gsummatr01lem3  21268  gsummatr01lem4  21269  gsummatr01  21270  slesolinvbi  21292  cpmatacl  21326  cpmatinvcl  21327  pmatcollpw2lem  21387  monmatcollpw  21389  pmatcollpwfi  21392  mp2pm2mplem4  21419  pm2mp  21435  cpmadugsumlemF  21486  cpmadugsumfi  21487  cpmadumatpoly  21493  cayhamlem4  21498  cayleyhamilton0  21499  cayleyhamiltonALT  21501  indistopon  21611  0ntr  21681  pnrmopn  21953  reftr  22124  kgenval  22145  pt1hmeo  22416  fmval  22553  fmf  22555  istmd  22684  istgp  22687  tsmsval2  22740  isxmet2d  22939  xpsxmetlem  22991  xpsmet  22994  blfvalps  22995  tmsval  23093  isnlm  23286  nmoleub  23342  idnghm  23354  blssioo  23405  blcvx  23408  icccvx  23556  pcorevlem  23632  isclm  23670  caufval  23880  iscms  23950  mbfsup  24267  i1f1  24293  dvexp3  24577  rolle  24589  dvivth  24609  deg1add  24699  0dgr  24837  coefv0  24840  elqaalem2  24911  dvradcnv  25011  abelthlem8  25029  efper  25067  logtayl  25245  abscxpbnd  25336  relogbcxpb  25367  logbgcd1irr  25374  dcubic2  25424  rlimcnp2  25546  cvxcl  25564  zetacvg  25594  lgamgulmlem2  25609  vmaval  25692  chtub  25790  logexprlim  25803  dchrsum2  25846  sumdchr2  25848  bposlem2  25863  lgsdir  25910  lgsne0  25913  lgsdirnn0  25922  lgsdinn0  25923  lgsquadlem2  25959  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgslem3d1  25981  2sqn0  26012  dchrvmasum2if  26075  dchrvmasumiflem1  26079  rpvmasum2  26090  pntpbnd1  26164  ostth2lem4  26214  trgcgrg  26303  tgcgr4  26319  ax5seglem1  26716  ax5seglem2  26717  ax5seglem5  26721  usgr1vr  27039  cplgr2vpr  27217  cplgr3v  27219  cusgrrusgr  27365  wlklenvm1  27405  wlk0prc  27437  wlksoneq1eq2  27448  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshwlkn0lem6  27595  crctcshlem4  27600  crctcsh  27604  wlkiswwlks1  27647  wwlksnext  27673  wwlksnextbi  27674  wwlksnextwrd  27677  midwwlks2s3  27733  clwlkclwwlklem2fv1  27775  clwlkclwwlklem2a4  27777  clwlkclwwlklem3  27781  clwwisshclwws  27795  erclwwlkeqlen  27799  clwwlkinwwlk  27820  clwwlkn2  27824  clwwlkf  27828  clwwlkf1  27830  eleclclwwlknlem2  27842  erclwwlkneqlen  27849  umgrhashecclwwlk  27859  eucrctshift  28024  eucrct2eupth  28026  fusgr2wsp2nb  28115  grpoidinvlem2  28284  vcz  28354  nvz  28448  lnon0  28577  ipasslem2  28611  htthlem  28696  hvpncan  28818  hiidge0  28877  normgt0  28906  hsn0elch  29027  shsel3  29094  spansneleq  29349  normcan  29355  h1datomi  29360  fh1  29397  spansncvi  29431  5oalem1  29433  5oalem3  29435  5oalem5  29437  3oalem2  29442  pjdsi  29491  kbpj  29735  0hmop  29762  0lnfn  29764  adj0  29773  nlelshi  29839  branmfn  29884  opsqrlem1  29919  hst1h  30006  mdsl0  30089  superpos  30133  sumdmdlem  30197  cdj3lem1  30213  f1od2  30459  xrpxdivcld  30613  xrge0npcan  30683  resvid2  30903  resvval2  30904  esumsnf  31325  esummulc1  31342  measxun2  31471  omsmeas  31583  sibfof  31600  probun  31679  signstfvn  31841  bnj517  32159  pthhashvtx  32376  ex-sategoelel  32670  mrsubfval  32757  msrval  32787  dfrdg2  33042  bj-prmoore  34409  bj-bary1lem1  34594  rdgeqoa  34653  finxpreclem2  34673  finxpreclem3  34676  matunitlindflem1  34890  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem14  34908  poimirlem15  34909  poimirlem17  34911  poimirlem20  34914  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  mblfinlem2  34932  mblfinlem3  34933  ismblfin  34935  mbfposadd  34941  itg2addnclem  34945  itg2addnclem3  34947  itg2addnc  34948  ftc1anclem8  34976  areacirc  34989  ismtyval  35080  ismrer1  35118  grposnOLD  35162  rabeq12f  35437  csbeq12  35438  iuneq12f  35443  lsatcv1  36186  glbconN  36515  atltcvr  36573  3dim2  36606  islln2a  36655  2at0mat0  36663  islpln2a  36686  islvol2aN  36730  pmodlem2  36985  pmapjat1  36991  pcl0bN  37061  osumclN  37105  pexmidALTN  37116  lhp2at0nle  37173  4atexlemunv  37204  cdleme18b  37430  cdleme31sn1  37519  cdleme31sde  37523  cdleme31sn2  37527  ltrniotavalbN  37722  trljco  37878  cdlemh  37955  cdlemk40t  38056  cdlemk40f  38057  cdleml9  38122  dihmeetlem3N  38443  dochkrshp  38524  dihprrn  38564  dihjat1  38567  dvh3dim  38584  dochkrsm  38596  dochexmid  38606  lcfl7lem  38637  lcfl9a  38643  lclkrlem1  38644  mapdspex  38806  mapdindp2  38859  mapdh6dN  38877  hdmap1l6d  38951  hdmap11lem2  38980  hdmap14lem4a  39009  hdmapip0  39053  hlhilset  39072  nnadd1com  39167  0prjspnrel  39276  jm2.26a  39604  radcnvrat  40653  sumsnd  41290  icccncfext  42177  fperdvper  42210  dvcosax  42218  ioodvbdlimc1lem1  42223  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  volioc  42264  itgiccshift  42272  stoweidlem34  42326  dirkercncflem2  42396  fourierdlem32  42431  fourierdlem41  42440  fourierdlem48  42446  fourierdlem64  42462  fourierdlem73  42471  fourierdlem79  42477  fourierdlem82  42480  fourierdlem97  42495  fourierdlem101  42499  fourierdlem109  42507  fourierdlem111  42509  fouriersw  42523  elaa2  42526  etransclem24  42550  etransclem25  42551  etransclem46  42572  nnfoctbdjlem  42744  ismeannd  42756  ndfatafv2undef  43418  fzopredsuc  43530  prproropf1olem3  43674  prproropf1olem4  43675  fmtnorec2lem  43711  2pwp1prmfmtno  43759  sfprmdvdsmersenne  43775  sgprmdvdsmersenne  43776  lighneallem2  43778  lighneallem3  43779  dfodd6  43809  dfeven4  43810  m1expevenALTV  43819  isomushgr  43998  isomuspgrlem2d  44003  clintopval  44118  lmod0rng  44146  zlidlring  44206  2zrngagrp  44221  rngcval  44240  ringcval  44286  dmmpossx2  44392  zlmodzxzscm  44412  zlmodzxzadd  44413  domnmsuppn0  44424  rmsuppss  44425  scmsuppss  44427  ply1mulgsumlem4  44450  ldepsprlem  44534  lincresunit2  44540  m1modmmod  44588  nn0sumshdiglemB  44687  affinecomb1  44696  itschlc0yqe  44754  itsclquadb  44770  2itscp  44775  0setrec  44813