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 457	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  sbcied2  3821  csbied2  3929  opthhausdorff0  5520  fun2ssres  6599  fcoi1  6771  fcoi2  6772  funssfv  6917  fvtp1  7207  nvof1o  7289  onuninsuci  7845  ot1stg  8008  ot2ndg  8009  el2xptp0  8041  mpomptsx  8069  dmmpossx  8071  fmpox  8072  2ndconst  8106  offsplitfpar  8124  mpoxopoveq  8225  wfrlem10OLD  8339  rdgeq12  8434  rdgsucmptnf  8450  frsucmptn  8460  oev2  8544  oesuclem  8546  oawordeulem  8575  om00  8596  omass  8601  omeulem1  8603  oeoa  8618  oeoe  8620  nnmass  8645  oaabs2  8670  omabs  8672  mapsnend  9061  omxpenlem  9098  sbthlem4  9111  sbthlem6  9113  fodomr  9153  ssenen  9176  fi0  9445  cantnfp1  9706  cnfcomlem  9724  ttrclselem2  9751  cardaleph  10114  cflim2  10288  axdc4lem  10480  fpwwe2lem11  10666  fpwwe2lem12  10667  rankcf  10802  inatsk  10803  ltrnq  11004  addclprlem1  11041  mulclprlem  11044  1idpr  11054  prlem936  11072  reclem3pr  11074  mulcmpblnrlem  11095  recexsrlem  11128  map2psrpr  11135  addid0  11665  subdivcomb2  11943  nnnn0addcl  12535  zindd  12696  qaddcl  12982  qmulcl  12984  qreccl  12986  xaddnemnf  13250  xaddnepnf  13251  xaddcom  13254  xnegdi  13262  xaddass  13263  xpncan  13265  xleadd1a  13267  xlt2add  13274  rexmul  13285  xmulgt0  13297  xmulge0  13298  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xadddi2  13311  modmuladd  13914  modm1p1mod0  13923  modfzo0difsn  13944  seqf1olem2  14043  expp1  14069  expneg  14070  expcllem  14073  mulexp  14102  expmul  14108  sqoddm1div8  14241  bcpasc  14316  hashrabsn01  14368  fseq1hash  14371  hashinfxadd  14380  hashfzo  14424  fnfz0hash  14441  ffzo0hash  14444  hashf1lem1  14451  hashf1lem1OLD  14452  hashge2el2dif  14477  hashdifsnp1  14493  lsw0  14551  ccatval1  14563  ccatval2  14564  swrdval  14629  ccatopth  14702  reuccatpfxs1  14733  splval  14737  repswswrd  14770  2cshwcshw  14812  s4dom  14906  wrdlen2i  14929  shftfn  15056  reim0b  15102  cjexp  15133  sqeqd  15149  fsumser  15712  sumsnf  15725  binomlem  15811  expcnv  15846  prodsn  15942  prodsnf  15944  bpolylem  16028  bpoly2  16037  bpoly3  16038  ef0lem  16058  dvdsnegb  16254  mod2eq1n2dvds  16327  m1expe  16354  m1expo  16355  m1exp1  16356  flodddiv4  16393  sadadd2lem2  16428  gcdabsOLD  16510  bezoutr1  16543  dvdslcm  16572  lcmeq0  16574  lcmcl  16575  lcmabs  16579  lcmgcdlem  16580  lcmdvds  16582  lcmf0val  16596  lcmftp  16610  lcmfunsnlem2  16614  mulgcddvds  16629  divgcdcoprmex  16640  pcge0  16834  pcadd  16861  pcmpt2  16865  prmreclem4  16891  ramval  16980  ramcl  17001  fvprmselelfz  17016  fvprmselgcd1  17017  ressid2  17216  ressval2  17217  mndind  18788  frmdval  18811  efmnd  18830  smndex1igid  18864  smndex1n0mnd  18872  mgm2nsgrplem3  18880  mulgfval  19033  mulgfvalALT  19034  mulgnn0subcl  19050  mulgnn0z  19064  cycsubm  19165  f1ghm0to0  19208  isga  19254  symgextfve  19386  symgfixf1  19404  f1omvdco2  19415  psgnsn  19487  odid  19505  gexid  19548  efgsval2  19700  frgpuptinv  19738  frgpup2  19743  dprdsn  20005  srgmulgass  20169  srgpcomp  20170  srgbinomlem4  20181  ringinvnzdiv  20249  rngcval  20563  ringcval  20592  isabvd  20712  issrng  20742  lmodvsmmulgdi  20792  mptscmfsupp0  20822  lvecinv  21013  lspdisj2  21027  lspfixed  21028  lspexch  21029  sralem  21073  sralemOLD  21074  srasca  21081  srascaOLD  21082  sravsca  21083  sravscaOLD  21084  sraip  21085  znval  21482  psgndiflemB  21549  isphl  21577  assamulgscmlem2  21850  mplval  21951  opsrval  22006  cply1mul  22240  gsummoncoe1  22252  evl1fval  22272  scmate  22456  scmatscm  22459  mdetdiagid  22546  mdetunilem7  22564  mdetuni0  22567  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  slesolinvbi  22627  cpmatacl  22662  cpmatinvcl  22663  pmatcollpw2lem  22723  monmatcollpw  22725  pmatcollpwfi  22728  mp2pm2mplem4  22755  pm2mp  22771  cpmadugsumlemF  22822  cpmadugsumfi  22823  cpmadumatpoly  22829  cayhamlem4  22834  cayleyhamilton0  22835  cayleyhamiltonALT  22837  indistopon  22948  0ntr  23019  pnrmopn  23291  reftr  23462  kgenval  23483  pt1hmeo  23754  fmval  23891  fmf  23893  istmd  24022  istgp  24025  tsmsval2  24078  isxmet2d  24277  xpsxmetlem  24329  xpsmet  24332  blfvalps  24333  tmsval  24433  isnlm  24636  nmoleub  24692  idnghm  24704  blssioo  24755  blcvx  24758  icccvx  24919  pcorevlem  24997  isclm  25035  caufval  25247  iscms  25317  mbfsup  25637  i1f1  25663  dvexp3  25954  rolle  25966  dvivth  25987  deg1add  26083  0dgr  26224  coefv0  26227  elqaalem2  26300  dvradcnv  26402  abelthlem8  26421  efper  26459  logtayl  26639  abscxpbnd  26733  relogbcxpb  26764  logbgcd1irr  26771  dcubic2  26821  rlimcnp2  26943  cvxcl  26962  zetacvg  26992  lgamgulmlem2  27007  vmaval  27090  chtub  27190  logexprlim  27203  dchrsum2  27246  sumdchr2  27248  bposlem2  27263  lgsdir  27310  lgsne0  27313  lgsdirnn0  27322  lgsdinn0  27323  lgsquadlem2  27359  2lgslem3a  27374  2lgslem3b  27375  2lgslem3c  27376  2lgslem3d  27377  2lgslem3a1  27378  2lgslem3b1  27379  2lgslem3c1  27380  2lgslem3d1  27381  2sqn0  27412  dchrvmasum2if  27475  dchrvmasumiflem1  27479  rpvmasum2  27490  pntpbnd1  27564  ostth2lem4  27614  trgcgrg  28391  tgcgr4  28407  ax5seglem1  28811  ax5seglem2  28812  ax5seglem5  28816  usgr1vr  29140  cplgr2vpr  29318  cplgr3v  29320  cusgrrusgr  29467  wlklenvm1  29508  wlk0prc  29540  wlksoneq1eq2  29550  crctcshwlkn0lem4  29696  crctcshwlkn0lem5  29697  crctcshwlkn0lem6  29698  crctcshlem4  29703  crctcsh  29707  wlkiswwlks1  29750  wwlksnext  29776  wwlksnextbi  29777  wwlksnextwrd  29780  midwwlks2s3  29835  clwlkclwwlklem2fv1  29877  clwlkclwwlklem2a4  29879  clwlkclwwlklem3  29883  clwwisshclwws  29897  erclwwlkeqlen  29901  clwwlkinwwlk  29922  clwwlkn2  29926  clwwlkf  29929  clwwlkf1  29931  eleclclwwlknlem2  29943  erclwwlkneqlen  29950  umgrhashecclwwlk  29960  eucrctshift  30125  eucrct2eupth  30127  fusgr2wsp2nb  30216  grpoidinvlem2  30387  vcz  30457  nvz  30551  lnon0  30680  ipasslem2  30714  htthlem  30799  hvpncan  30921  hiidge0  30980  normgt0  31009  hsn0elch  31130  shsel3  31197  spansneleq  31452  normcan  31458  h1datomi  31463  fh1  31500  spansncvi  31534  5oalem1  31536  5oalem3  31538  5oalem5  31540  3oalem2  31545  pjdsi  31594  kbpj  31838  0hmop  31865  0lnfn  31867  adj0  31876  nlelshi  31942  branmfn  31987  opsqrlem1  32022  hst1h  32109  mdsl0  32192  superpos  32236  sumdmdlem  32300  cdj3lem1  32316  f1od2  32585  xrpxdivcld  32743  xrge0npcan  32839  rlocf1  33063  resvid2  33138  resvval2  33139  qsdrng  33309  r1pquslmic  33412  esumsnf  33814  esummulc1  33831  measxun2  33960  omsmeas  34074  sibfof  34091  probun  34170  signstfvn  34332  bnj517  34647  pthhashvtx  34868  ex-sategoelel  35162  mrsubfval  35249  msrval  35279  dfrdg2  35522  bj-prmoore  36725  bj-bary1lem1  36921  rdgeqoa  36980  finxpreclem2  37000  finxpreclem3  37003  matunitlindflem1  37220  poimirlem1  37225  poimirlem2  37226  poimirlem3  37227  poimirlem4  37228  poimirlem5  37229  poimirlem6  37230  poimirlem7  37231  poimirlem10  37234  poimirlem11  37235  poimirlem12  37236  poimirlem14  37238  poimirlem15  37239  poimirlem17  37241  poimirlem20  37244  poimirlem22  37246  poimirlem23  37247  poimirlem24  37248  poimirlem25  37249  poimirlem26  37250  poimirlem27  37251  mblfinlem2  37262  mblfinlem3  37263  ismblfin  37265  mbfposadd  37271  itg2addnclem  37275  itg2addnclem3  37277  itg2addnc  37278  ftc1anclem8  37304  areacirc  37317  ismtyval  37404  ismrer1  37442  grposnOLD  37486  rabeq12f  37761  csbeq12  37762  iuneq12f  37767  lsatcv1  38650  glbconN  38979  glbconNOLD  38980  atltcvr  39038  3dim2  39071  islln2a  39120  2at0mat0  39128  islpln2a  39151  islvol2aN  39195  pmodlem2  39450  pmapjat1  39456  pcl0bN  39526  osumclN  39570  pexmidALTN  39581  lhp2at0nle  39638  4atexlemunv  39669  cdleme18b  39895  cdleme31sn1  39984  cdleme31sde  39988  cdleme31sn2  39992  ltrniotavalbN  40187  trljco  40343  cdlemh  40420  cdlemk40t  40521  cdlemk40f  40522  cdleml9  40587  dihmeetlem3N  40908  dochkrshp  40989  dihprrn  41029  dihjat1  41032  dvh3dim  41049  dochkrsm  41061  dochexmid  41071  lcfl7lem  41102  lcfl9a  41108  lclkrlem1  41109  mapdspex  41271  mapdindp2  41324  mapdh6dN  41342  hdmap1l6d  41416  hdmap11lem2  41445  hdmap14lem4a  41474  hdmapip0  41518  hlhilset  41537  nnadd1com  41977  sn-negex12  42106  prjspner1  42185  0prjspnrel  42186  jm2.26a  42563  onov0suclim  42845  oe0suclim  42848  cantnfresb  42895  onmcl  42902  omcl2  42904  tfsconcatun  42908  naddwordnexlem4  42973  mnringmulrcld  43807  radcnvrat  43893  sumsnd  44530  icccncfext  45413  fperdvper  45445  dvcosax  45452  ioodvbdlimc1lem1  45457  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  volioc  45498  itgiccshift  45506  stoweidlem34  45560  dirkercncflem2  45630  fourierdlem32  45665  fourierdlem41  45674  fourierdlem48  45680  fourierdlem64  45696  fourierdlem73  45705  fourierdlem79  45711  fourierdlem82  45714  fourierdlem97  45729  fourierdlem101  45733  fourierdlem109  45741  fourierdlem111  45743  fouriersw  45757  elaa2  45760  etransclem24  45784  etransclem25  45785  etransclem46  45806  nnfoctbdjlem  45981  ismeannd  45993  smfpimltxr  46273  smfpimgtxr  46306  ndfatafv2undef  46730  fzopredsuc  46841  prproropf1olem3  46982  prproropf1olem4  46983  fmtnorec2lem  47019  2pwp1prmfmtno  47067  sfprmdvdsmersenne  47080  sgprmdvdsmersenne  47081  lighneallem2  47083  lighneallem3  47084  dfodd6  47114  dfeven4  47115  m1expevenALTV  47124  gricushgr  47369  clintopval  47452  lmod0rng  47477  zlidlring  47482  2zrngagrp  47497  dmmpossx2  47586  zlmodzxzscm  47607  zlmodzxzadd  47608  domnmsuppn0  47619  rmsuppss  47620  scmsuppss  47622  ply1mulgsumlem4  47643  ldepsprlem  47726  lincresunit2  47732  m1modmmod  47780  nn0sumshdiglemB  47879  2arymptfv  47909  ackval42  47955  affinecomb1  47961  itschlc0yqe  48019  itsclquadb  48035  2itscp  48040  0setrec  48321