Theorem sylan9eqr 2790

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

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

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  sbcied2  3782  csbied2  3883  opthhausdorff0  5463  fun2ssres  6534  fcoi1  6705  fcoi2  6706  funssfv  6852  fvtp1  7138  nvof1o  7223  onuninsuci  7779  ot1stg  7944  ot2ndg  7945  el2xptp0  7977  mpomptsx  8005  dmmpossx  8007  fmpox  8008  2ndconst  8040  offsplitfpar  8058  mpoxopoveq  8158  rdgeq12  8341  rdgsucmptnf  8357  frsucmptn  8367  oev2  8447  oesuclem  8449  oawordeulem  8478  om00  8499  omass  8504  omeulem1  8506  oeoa  8521  oeoe  8523  nnmass  8548  oaabs2  8573  omabs  8575  mapsnend  8969  omxpenlem  9002  sbthlem4  9014  sbthlem6  9016  fodomr  9052  ssenen  9075  fodomfir  9223  fi0  9315  cantnfp1  9582  cnfcomlem  9600  ttrclselem2  9627  cardaleph  9991  cflim2  10165  axdc4lem  10357  fpwwe2lem11  10543  fpwwe2lem12  10544  rankcf  10679  inatsk  10680  ltrnq  10881  addclprlem1  10918  mulclprlem  10921  1idpr  10931  prlem936  10949  reclem3pr  10951  mulcmpblnrlem  10972  recexsrlem  11005  map2psrpr  11012  addid0  11547  subdivcomb2  11828  nnnn0addcl  12422  zindd  12584  qaddcl  12869  qmulcl  12871  qreccl  12873  xaddnemnf  13142  xaddnepnf  13143  xaddcom  13146  xnegdi  13154  xaddass  13155  xpncan  13157  xleadd1a  13159  xlt2add  13166  rexmul  13177  xmulgt0  13189  xmulge0  13190  xmulasslem3  13192  xlemul1a  13194  xadddilem  13200  xadddi2  13203  modmuladd  13827  modm1p1mod0  13836  modfzo0difsn  13857  seqf1olem2  13956  expp1  13982  expneg  13983  expcllem  13986  mulexp  14015  expmul  14021  sqoddm1div8  14157  bcpasc  14235  hashrabsn01  14287  fseq1hash  14290  hashinfxadd  14299  hashfzo  14343  fnfz0hash  14360  ffzo0hash  14363  hashf1lem1  14369  hashge2el2dif  14394  hash3tpexb  14408  hashdifsnp1  14420  lsw0  14479  ccatval1  14491  ccatval2  14492  swrdval  14558  ccatopth  14630  reuccatpfxs1  14661  splval  14665  repswswrd  14698  2cshwcshw  14739  s4dom  14833  wrdlen2i  14856  shftfn  14987  reim0b  15033  cjexp  15064  sqeqd  15080  fsumser  15644  sumsnf  15657  binomlem  15743  expcnv  15778  prodsn  15876  prodsnf  15878  bpolylem  15962  bpoly2  15971  bpoly3  15972  ef0lem  15992  dvdsnegb  16191  mod2eq1n2dvds  16265  m1expe  16292  m1expo  16293  m1exp1  16294  flodddiv4  16333  sadadd2lem2  16368  bezoutr1  16487  dvdslcm  16516  lcmeq0  16518  lcmcl  16519  lcmabs  16523  lcmgcdlem  16524  lcmdvds  16526  lcmf0val  16540  lcmftp  16554  lcmfunsnlem2  16558  mulgcddvds  16573  divgcdcoprmex  16584  pcge0  16781  pcadd  16808  pcmpt2  16812  prmreclem4  16838  ramval  16927  ramcl  16948  fvprmselelfz  16963  fvprmselgcd1  16964  ressid2  17152  ressval2  17153  mndind  18744  frmdval  18767  efmnd  18786  smndex1igid  18820  smndex1n0mnd  18828  mgm2nsgrplem3  18836  mulgfval  18990  mulgfvalALT  18991  mulgnn0subcl  19008  mulgnn0z  19022  cycsubm  19122  f1ghm0to0  19165  isga  19211  symgextfve  19339  symgfixf1  19357  f1omvdco2  19368  psgnsn  19440  odid  19458  gexid  19501  efgsval2  19653  frgpuptinv  19691  frgpup2  19696  dprdsn  19958  srgmulgass  20143  srgpcomp  20144  srgbinomlem4  20155  ringinvnzdiv  20227  rngcval  20542  ringcval  20571  isabvd  20736  issrng  20768  lmodvsmmulgdi  20839  mptscmfsupp0  20869  lvecinv  21059  lspdisj2  21073  lspfixed  21074  lspexch  21075  sralem  21119  srasca  21123  sravsca  21124  sraip  21125  znval  21481  psgndiflemB  21546  isphl  21574  assamulgscmlem2  21847  mplval  21935  opsrval  21992  psdmvr  22103  cply1mul  22231  gsummoncoe1  22243  evl1fval  22263  scmate  22445  scmatscm  22448  mdetdiagid  22535  mdetunilem7  22553  mdetuni0  22556  gsummatr01lem3  22592  gsummatr01lem4  22593  gsummatr01  22594  slesolinvbi  22616  cpmatacl  22651  cpmatinvcl  22652  pmatcollpw2lem  22712  monmatcollpw  22714  pmatcollpwfi  22717  mp2pm2mplem4  22744  pm2mp  22760  cpmadugsumlemF  22811  cpmadugsumfi  22812  cpmadumatpoly  22818  cayhamlem4  22823  cayleyhamilton0  22824  cayleyhamiltonALT  22826  indistopon  22936  0ntr  23006  pnrmopn  23278  reftr  23449  kgenval  23470  pt1hmeo  23741  fmval  23878  fmf  23880  istmd  24009  istgp  24012  tsmsval2  24065  isxmet2d  24262  xpsxmetlem  24314  xpsmet  24317  blfvalps  24318  tmsval  24416  isnlm  24610  nmoleub  24666  idnghm  24678  blssioo  24730  blcvx  24733  icccvx  24895  pcorevlem  24973  isclm  25011  caufval  25222  iscms  25292  mbfsup  25612  i1f1  25638  dvexp3  25929  rolle  25941  dvivth  25962  deg1add  26055  0dgr  26197  coefv0  26200  elqaalem2  26275  dvradcnv  26377  abelthlem8  26396  efper  26435  logtayl  26616  abscxpbnd  26710  relogbcxpb  26744  logbgcd1irr  26751  dcubic2  26801  rlimcnp2  26923  cvxcl  26942  zetacvg  26972  lgamgulmlem2  26987  vmaval  27070  chtub  27170  logexprlim  27183  dchrsum2  27226  sumdchr2  27228  bposlem2  27243  lgsdir  27290  lgsne0  27293  lgsdirnn0  27302  lgsdinn0  27303  lgsquadlem2  27339  2lgslem3a  27354  2lgslem3b  27355  2lgslem3c  27356  2lgslem3d  27357  2lgslem3a1  27358  2lgslem3b1  27359  2lgslem3c1  27360  2lgslem3d1  27361  2sqn0  27392  dchrvmasum2if  27455  dchrvmasumiflem1  27459  rpvmasum2  27470  pntpbnd1  27544  ostth2lem4  27594  expsp1  28372  trgcgrg  28513  tgcgr4  28529  ax5seglem1  28927  ax5seglem2  28928  ax5seglem5  28932  usgr1vr  29254  cplgr2vpr  29432  cplgr3v  29434  cusgrrusgr  29581  wlklenvm1  29621  wlk0prc  29652  wlksoneq1eq2  29662  crctcshwlkn0lem4  29812  crctcshwlkn0lem5  29813  crctcshwlkn0lem6  29814  crctcshlem4  29819  crctcsh  29823  wlkiswwlks1  29866  wwlksnext  29892  wwlksnextbi  29893  wwlksnextwrd  29896  midwwlks2s3  29951  clwlkclwwlklem2fv1  29996  clwlkclwwlklem2a4  29998  clwlkclwwlklem3  30002  clwwisshclwws  30016  erclwwlkeqlen  30020  clwwlkinwwlk  30041  clwwlkn2  30045  clwwlkf  30048  clwwlkf1  30050  eleclclwwlknlem2  30062  erclwwlkneqlen  30069  umgrhashecclwwlk  30079  eucrctshift  30244  eucrct2eupth  30246  fusgr2wsp2nb  30335  grpoidinvlem2  30506  vcz  30576  nvz  30670  lnon0  30799  ipasslem2  30833  htthlem  30918  hvpncan  31040  hiidge0  31099  normgt0  31128  hsn0elch  31249  shsel3  31316  spansneleq  31571  normcan  31577  h1datomi  31582  fh1  31619  spansncvi  31653  5oalem1  31655  5oalem3  31657  5oalem5  31659  3oalem2  31664  pjdsi  31713  kbpj  31957  0hmop  31984  0lnfn  31986  adj0  31995  nlelshi  32061  branmfn  32106  opsqrlem1  32141  hst1h  32228  mdsl0  32311  superpos  32355  sumdmdlem  32419  cdj3lem1  32435  f1od2  32726  xrpxdivcld  32944  xrge0npcan  33030  elrgspnlem2  33253  rlocf1  33283  resvid2  33339  resvval2  33340  qsdrng  33506  r1pquslmic  33620  mplvrpmmhm  33639  mplvrpmrhm  33640  esplyfval0  33650  vietalem  33663  rtelextdg2lem  33811  esumsnf  34149  esummulc1  34166  measxun2  34295  omsmeas  34408  sibfof  34425  probun  34504  signstfvn  34654  bnj517  34969  pthhashvtx  35244  ex-sategoelel  35537  mrsubfval  35624  msrval  35654  dfrdg2  35909  itgeq12i  36322  bj-prmoore  37232  bj-bary1lem1  37428  rdgeqoa  37487  finxpreclem2  37507  finxpreclem3  37510  matunitlindflem1  37729  poimirlem1  37734  poimirlem2  37735  poimirlem3  37736  poimirlem4  37737  poimirlem5  37738  poimirlem6  37739  poimirlem7  37740  poimirlem10  37743  poimirlem11  37744  poimirlem12  37745  poimirlem14  37747  poimirlem15  37748  poimirlem17  37750  poimirlem20  37753  poimirlem22  37755  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  mblfinlem2  37771  mblfinlem3  37772  ismblfin  37774  mbfposadd  37780  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  ftc1anclem8  37813  areacirc  37826  ismtyval  37913  ismrer1  37951  grposnOLD  37995  rabeq12f  38270  csbeq12  38271  iuneq12f  38276  lsatcv1  39220  glbconN  39549  atltcvr  39607  3dim2  39640  islln2a  39689  2at0mat0  39697  islpln2a  39720  islvol2aN  39764  pmodlem2  40019  pmapjat1  40025  pcl0bN  40095  osumclN  40139  pexmidALTN  40150  lhp2at0nle  40207  4atexlemunv  40238  cdleme18b  40464  cdleme31sn1  40553  cdleme31sde  40557  cdleme31sn2  40561  ltrniotavalbN  40756  trljco  40912  cdlemh  40989  cdlemk40t  41090  cdlemk40f  41091  cdleml9  41156  dihmeetlem3N  41477  dochkrshp  41558  dihprrn  41598  dihjat1  41601  dvh3dim  41618  dochkrsm  41630  dochexmid  41640  lcfl7lem  41671  lcfl9a  41677  lclkrlem1  41678  mapdspex  41840  mapdindp2  41893  mapdh6dN  41911  hdmap1l6d  41985  hdmap11lem2  42014  hdmap14lem4a  42043  hdmapip0  42087  hlhilset  42106  nnadd1com  42437  mulgt0b2d  42648  fiabv  42706  prjspner1  42784  0prjspnrel  42785  jm2.26a  43157  onov0suclim  43431  oe0suclim  43434  cantnfresb  43481  onmcl  43488  omcl2  43490  tfsconcatun  43494  naddwordnexlem4  43558  mnringmulrcld  44385  radcnvrat  44471  sumsnd  45187  icccncfext  46047  fperdvper  46079  dvcosax  46086  ioodvbdlimc1lem1  46091  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  volioc  46132  itgiccshift  46140  stoweidlem34  46194  dirkercncflem2  46264  fourierdlem32  46299  fourierdlem41  46308  fourierdlem48  46314  fourierdlem64  46330  fourierdlem73  46339  fourierdlem79  46345  fourierdlem82  46348  fourierdlem97  46363  fourierdlem101  46367  fourierdlem109  46375  fourierdlem111  46377  fouriersw  46391  elaa2  46394  etransclem24  46418  etransclem25  46419  etransclem46  46440  nnfoctbdjlem  46615  ismeannd  46627  smfpimltxr  46907  smfpimgtxr  46940  ndfatafv2undef  47374  fzopredsuc  47485  m1modmmod  47520  modlt0b  47525  prproropf1olem3  47667  prproropf1olem4  47668  fmtnorec2lem  47704  2pwp1prmfmtno  47752  sfprmdvdsmersenne  47765  sgprmdvdsmersenne  47766  lighneallem2  47768  lighneallem3  47769  dfodd6  47799  dfeven4  47800  m1expevenALTV  47809  isubgredg  48028  upgrimwlklem5  48063  gricushgr  48079  stgrusgra  48121  isubgr3stgrlem8  48135  clintopval  48366  lmod0rng  48391  zlidlring  48396  2zrngagrp  48411  dmmpossx2  48499  zlmodzxzscm  48519  zlmodzxzadd  48520  domnmsuppn0  48531  rmsuppss  48532  scmsuppss  48533  ply1mulgsumlem4  48551  ldepsprlem  48634  lincresunit2  48640  nn0sumshdiglemB  48782  2arymptfv  48812  ackval42  48858  affinecomb1  48864  itschlc0yqe  48922  itsclquadb  48938  2itscp  48943  incat  49762  0setrec  49865