Theorem sylan9eqr 2862

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  sbcied2  3671  csbied2  3756  opthhausdorff0  5173  fun2ssres  6145  fcoi1  6293  fcoi2  6294  funssfv  6429  fvtp1  6685  nvof1o  6760  onuninsuci  7270  ot1stg  7412  ot2ndg  7413  el2xptp0  7444  mpt2mptsx  7466  dmmpt2ssx  7468  fmpt2x  7469  2ndconst  7500  mpt2xopoveq  7580  wfrlem10  7660  rdgeq12  7745  rdgsucmptnf  7761  frsucmptn  7770  oev2  7840  oesuclem  7842  oawordeulem  7871  om00  7892  omass  7897  oeoa  7914  oeoe  7916  nnmass  7941  oaabs2  7962  omabs  7964  omxpenlem  8300  sbthlem4  8312  sbthlem6  8314  fodomr  8350  ssenen  8373  fi0  8565  cantnfp1  8825  cnfcomlem  8843  cardaleph  9195  cflim2  9370  axdc4lem  9562  fpwwe2lem12  9748  fpwwe2lem13  9749  rankcf  9884  inatsk  9885  ltrnq  10086  addclprlem1  10123  mulclprlem  10126  1idpr  10136  prlem936  10154  reclem3pr  10156  mulcmpblnrlem  10176  recexsrlem  10209  map2psrpr  10216  addid0  10735  nnnn0addcl  11589  zindd  11744  qaddcl  12023  qmulcl  12025  qreccl  12027  xaddnemnf  12285  xaddnepnf  12286  xaddcom  12289  xnegdi  12296  xaddass  12297  xpncan  12299  xleadd1a  12301  xlt2add  12308  rexmul  12319  xmulgt0  12331  xmulge0  12332  xmulasslem3  12334  xlemul1a  12336  xadddilem  12342  xadddi2  12345  modmuladd  12936  modm1p1mod0  12945  modfzo0difsn  12966  seqf1olem2  13064  expp1  13090  expneg  13091  expcllem  13094  mulexp  13122  expmul  13128  sqoddm1div8  13251  bcpasc  13328  hashrabsn01  13380  fseq1hash  13383  hashinfxadd  13392  hashfzo  13433  fnfz0hash  13447  ffzo0hash  13450  hashf1lem1  13456  hashge2el2dif  13479  hashdifsnp1  13495  lsw0  13564  ccatval1  13574  ccatval2  13575  swrdval  13640  reuccats1  13704  splval  13726  repswswrd  13755  2cshwcshw  13795  s4dom  13888  wrdlen2i  13911  shftfn  14036  reim0b  14082  cjexp  14113  sqeqd  14129  fsumser  14684  sumsnf  14696  sumsn  14698  binomlem  14783  expcnv  14818  prodsn  14913  prodsnf  14915  bpolylem  14999  bpoly2  15008  bpoly3  15009  ef0lem  15029  dvdsnegb  15222  mod2eq1n2dvds  15291  m1expe  15311  m1expo  15312  m1exp1  15313  flodddiv4  15356  sadadd2lem2  15391  gcdabs  15469  bezoutr1  15501  dvdslcm  15530  lcmeq0  15532  lcmcl  15533  lcmabs  15537  lcmgcdlem  15538  lcmdvds  15540  lcmf0val  15554  lcmftp  15568  lcmfunsnlem2  15572  mulgcddvds  15587  divgcdcoprmex  15598  pcge0  15783  pcadd  15810  pcmpt2  15814  prmreclem4  15840  ramval  15929  ramcl  15950  fvprmselelfz  15965  fvprmselgcd1  15966  ressid2  16139  ressval2  16140  mrcmndind  17571  frmdval  17593  mgm2nsgrplem3  17612  mulgfval  17747  mulgnn0subcl  17759  mulgnn0z  17771  isga  17925  symgval  18000  symgextfve  18040  symgfixf1  18058  f1omvdco2  18069  psgnsn  18141  odid  18158  gexid  18197  frgpuptinv  18385  frgpup2  18390  dprdsn  18637  srgmulgass  18733  srgpcomp  18734  srgbinomlem4  18745  ringinvnzdiv  18795  f1rhm0to0  18944  f1rhm0to0ALT  18945  isabvd  19024  issrng  19054  lmodvsmmulgdi  19102  mptscmfsupp0  19132  lvecinv  19320  lspdisj2  19334  lspfixed  19335  lspfixedOLD  19336  lspexch  19337  sralem  19386  srasca  19390  sravsca  19391  sraip  19392  assamulgscmlem2  19558  mplval  19637  opsrval  19683  cply1mul  19872  gsummoncoe1  19882  evl1fval  19900  znval  20091  psgndiflemB  20154  isphl  20183  scmate  20527  scmatscm  20530  mdetdiagid  20617  mdetunilem7  20635  mdetuni0  20638  gsummatr01lem3  20675  gsummatr01lem4  20676  gsummatr01  20677  slesolinvbi  20699  cpmatacl  20734  cpmatinvcl  20735  pmatcollpw2lem  20795  monmatcollpw  20797  pmatcollpwfi  20800  mp2pm2mplem4  20827  pm2mp  20843  cpmadugsumlemF  20894  cpmadugsumfi  20895  cpmadumatpoly  20901  cayhamlem4  20906  cayleyhamilton0  20907  cayleyhamiltonALT  20909  indistopon  21019  0ntr  21089  pnrmopn  21361  reftr  21531  kgenval  21552  pt1hmeo  21823  fmval  21960  fmf  21962  istmd  22091  istgp  22094  tsmsval2  22146  isxmet2d  22345  xpsxmetlem  22397  xpsmet  22400  blfvalps  22401  tmsval  22499  isnlm  22692  nmoleub  22748  idnghm  22760  blssioo  22811  blcvx  22814  icccvx  22962  pcorevlem  23038  isclm  23076  caufval  23285  iscms  23354  mbfsup  23645  i1f1  23671  dvexp3  23955  rolle  23967  dvivth  23987  deg1add  24077  0dgr  24215  coefv0  24218  elqaalem2  24289  dvradcnv  24389  abelthlem8  24407  efper  24446  logtayl  24620  abscxpbnd  24708  relogbcxpb  24739  dcubic2  24785  rlimcnp2  24907  cvxcl  24925  zetacvg  24955  lgamgulmlem2  24970  vmaval  25053  chtub  25151  logexprlim  25164  dchrsum2  25207  sumdchr2  25209  bposlem2  25224  lgsdir  25271  lgsne0  25274  lgsdirnn0  25283  lgsdinn0  25284  lgsquadlem2  25320  2lgslem3a  25335  2lgslem3b  25336  2lgslem3c  25337  2lgslem3d  25338  2lgslem3a1  25339  2lgslem3b1  25340  2lgslem3c1  25341  2lgslem3d1  25342  dchrvmasum2if  25400  dchrvmasumiflem1  25404  rpvmasum2  25415  pntpbnd1  25489  ostth2lem4  25539  trgcgrg  25624  ax5seglem1  26022  ax5seglem2  26023  ax5seglem5  26027  usgr1vr  26363  cplgr2vpr  26557  cplgr3v  26559  cusgrrusgr  26705  wlklenvm1  26745  wlk0prc  26778  wlksoneq1eq2  26788  crctcshwlkn0lem4  26934  crctcshwlkn0lem5  26935  crctcshwlkn0lem6  26936  crctcshlem4  26941  crctcsh  26945  wlkiswwlks1  26994  wwlksnextbi  27031  wwlksnextwrd  27034  midwwlks2s3  27092  clwlkclwwlklem2fv1  27138  clwlkclwwlklem2a4  27140  clwlkclwwlklem3  27144  clwwisshclwws  27158  erclwwlkeqlen  27162  clwwlkinwwlk  27189  clwwlkn2  27193  clwwlkf  27196  clwwlkf1  27198  wwlksext2clwwlkOLD  27208  eleclclwwlknlem2  27212  erclwwlkneqlen  27219  umgrhashecclwwlk  27229  eucrctshift  27416  eucrct2eupth  27418  fusgr2wsp2nb  27509  grpoidinvlem2  27688  vcz  27758  nvz  27852  lnon0  27981  ipasslem2  28015  htthlem  28102  hvpncan  28224  hiidge0  28283  normgt0  28312  hsn0elch  28433  shsel3  28502  spansneleq  28757  normcan  28763  h1datomi  28768  fh1  28805  spansncvi  28839  5oalem1  28841  5oalem3  28843  5oalem5  28845  3oalem2  28850  pjdsi  28899  kbpj  29143  0hmop  29170  0lnfn  29172  adj0  29181  nlelshi  29247  branmfn  29292  opsqrlem1  29327  hst1h  29414  mdsl0  29497  superpos  29541  sumdmdlem  29605  cdj3lem1  29621  f1od2  29826  xrpxdivcld  29968  2sqn0  29971  xrge0npcan  30019  resvid2  30153  resvval2  30154  esumsnf  30451  esummulc1  30468  measxun2  30598  omsmeas  30710  sibfof  30727  probun  30806  bnj517  31278  mrsubfval  31728  msrval  31758  subdivcomb2  31934  dfrdg2  32021  bj-bary1lem1  33478  rdgeqoa  33534  finxpreclem2  33543  finxpreclem3  33546  matunitlindflem1  33718  poimirlem1  33723  poimirlem2  33724  poimirlem3  33725  poimirlem4  33726  poimirlem5  33727  poimirlem6  33728  poimirlem7  33729  poimirlem10  33732  poimirlem11  33733  poimirlem12  33734  poimirlem14  33736  poimirlem15  33737  poimirlem17  33739  poimirlem20  33742  poimirlem22  33744  poimirlem23  33745  poimirlem24  33746  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  mblfinlem2  33760  mblfinlem3  33761  ismblfin  33763  mbfposadd  33769  itg2addnclem  33773  itg2addnclem3  33775  itg2addnc  33776  ftc1anclem8  33804  areacirc  33817  ismtyval  33910  ismrer1  33948  grposnOLD  33992  rabeq12f  34275  csbeq12  34276  iuneq12f  34282  lsatcv1  34828  glbconN  35157  atltcvr  35215  3dim2  35248  islln2a  35297  2at0mat0  35305  islpln2a  35328  islvol2aN  35372  pmodlem2  35627  pmapjat1  35633  pcl0bN  35703  osumclN  35747  pexmidALTN  35758  lhp2at0nle  35815  4atexlemunv  35846  cdleme18b  36073  cdleme31sn1  36162  cdleme31sde  36166  cdleme31sn2  36170  ltrniotavalbN  36365  trljco  36521  cdlemh  36598  cdlemk40t  36699  cdlemk40f  36700  cdleml9  36765  dihmeetlem3N  37086  dochkrshp  37167  dihprrn  37207  dihjat1  37210  dvh3dim  37227  dochkrsm  37239  dochexmid  37249  lcfl7lem  37280  lcfl9a  37286  lclkrlem1  37287  mapdspex  37449  mapdindp2  37502  mapdh6dN  37520  hdmap1l6d  37594  hdmap11lem2  37623  hdmap14lem4a  37652  hdmapip0  37696  hlhilset  37715  jm2.26a  38068  radcnvrat  39013  sumsnd  39679  icccncfext  40580  fperdvper  40613  dvcosax  40621  ioodvbdlimc1lem1  40626  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  volioc  40667  itgiccshift  40675  stoweidlem34  40730  dirkercncflem2  40800  fourierdlem32  40835  fourierdlem41  40844  fourierdlem48  40850  fourierdlem64  40866  fourierdlem73  40875  fourierdlem79  40881  fourierdlem82  40884  fourierdlem97  40899  fourierdlem101  40903  fourierdlem109  40911  fourierdlem111  40913  fouriersw  40927  elaa2  40930  etransclem24  40954  etransclem25  40955  etransclem46  40976  nnfoctbdjlem  41151  ismeannd  41163  ndfatafv2undef  41801  fzopredsuc  41908  fmtnorec2lem  42029  2pwp1prmfmtno  42079  sfprmdvdsmersenne  42095  sgprmdvdsmersenne  42096  lighneallem2  42098  lighneallem3  42099  dfodd6  42125  dfeven4  42126  m1expevenALTV  42135  clintopval  42408  lmod0rng  42436  zlidlring  42496  2zrngagrp  42511  rngcval  42530  ringcval  42576  dmmpt2ssx2  42683  zlmodzxzscm  42703  zlmodzxzadd  42704  domnmsuppn0  42718  rmsuppss  42719  scmsuppss  42721  ply1mulgsumlem4  42745  ldepsprlem  42829  lincresunit2  42835  m1modmmod  42884  nn0sumshdiglemB  42982  0setrec  43018