Theorem sylan9eqr 2794

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  sbcied2  3823  csbied2  3932  opthhausdorff0  5517  fun2ssres  6590  fcoi1  6762  fcoi2  6763  funssfv  6909  fvtp1  7192  nvof1o  7274  onuninsuci  7825  ot1stg  7985  ot2ndg  7986  el2xptp0  8018  mpomptsx  8046  dmmpossx  8048  fmpox  8049  2ndconst  8083  offsplitfpar  8101  mpoxopoveq  8200  wfrlem10OLD  8314  rdgeq12  8409  rdgsucmptnf  8425  frsucmptn  8435  oev2  8519  oesuclem  8521  oawordeulem  8550  om00  8571  omass  8576  omeulem1  8578  oeoa  8593  oeoe  8595  nnmass  8620  oaabs2  8644  omabs  8646  mapsnend  9032  omxpenlem  9069  sbthlem4  9082  sbthlem6  9084  fodomr  9124  ssenen  9147  fi0  9411  cantnfp1  9672  cnfcomlem  9690  ttrclselem2  9717  cardaleph  10080  cflim2  10254  axdc4lem  10446  fpwwe2lem11  10632  fpwwe2lem12  10633  rankcf  10768  inatsk  10769  ltrnq  10970  addclprlem1  11007  mulclprlem  11010  1idpr  11020  prlem936  11038  reclem3pr  11040  mulcmpblnrlem  11061  recexsrlem  11094  map2psrpr  11101  addid0  11629  subdivcomb2  11906  nnnn0addcl  12498  zindd  12659  qaddcl  12945  qmulcl  12947  qreccl  12949  xaddnemnf  13211  xaddnepnf  13212  xaddcom  13215  xnegdi  13223  xaddass  13224  xpncan  13226  xleadd1a  13228  xlt2add  13235  rexmul  13246  xmulgt0  13258  xmulge0  13259  xmulasslem3  13261  xlemul1a  13263  xadddilem  13269  xadddi2  13272  modmuladd  13874  modm1p1mod0  13883  modfzo0difsn  13904  seqf1olem2  14004  expp1  14030  expneg  14031  expcllem  14034  mulexp  14063  expmul  14069  sqoddm1div8  14202  bcpasc  14277  hashrabsn01  14329  fseq1hash  14332  hashinfxadd  14341  hashfzo  14385  fnfz0hash  14401  ffzo0hash  14404  hashf1lem1  14411  hashf1lem1OLD  14412  hashge2el2dif  14437  hashdifsnp1  14453  lsw0  14511  ccatval1  14523  ccatval2  14524  swrdval  14589  ccatopth  14662  reuccatpfxs1  14693  splval  14697  repswswrd  14730  2cshwcshw  14772  s4dom  14866  wrdlen2i  14889  shftfn  15016  reim0b  15062  cjexp  15093  sqeqd  15109  fsumser  15672  sumsnf  15685  binomlem  15771  expcnv  15806  prodsn  15902  prodsnf  15904  bpolylem  15988  bpoly2  15997  bpoly3  15998  ef0lem  16018  dvdsnegb  16213  mod2eq1n2dvds  16286  m1expe  16313  m1expo  16314  m1exp1  16315  flodddiv4  16352  sadadd2lem2  16387  gcdabsOLD  16469  bezoutr1  16502  dvdslcm  16531  lcmeq0  16533  lcmcl  16534  lcmabs  16538  lcmgcdlem  16539  lcmdvds  16541  lcmf0val  16555  lcmftp  16569  lcmfunsnlem2  16573  mulgcddvds  16588  divgcdcoprmex  16599  pcge0  16791  pcadd  16818  pcmpt2  16822  prmreclem4  16848  ramval  16937  ramcl  16958  fvprmselelfz  16973  fvprmselgcd1  16974  ressid2  17173  ressval2  17174  mndind  18705  frmdval  18728  efmnd  18747  smndex1igid  18781  smndex1n0mnd  18789  mgm2nsgrplem3  18797  mulgfval  18946  mulgfvalALT  18947  mulgnn0subcl  18961  mulgnn0z  18975  cycsubm  19073  isga  19149  symgextfve  19281  symgfixf1  19299  f1omvdco2  19310  psgnsn  19382  odid  19400  gexid  19443  efgsval2  19595  frgpuptinv  19633  frgpup2  19638  dprdsn  19900  srgmulgass  20033  srgpcomp  20034  srgbinomlem4  20045  ringinvnzdiv  20106  f1ghm0to0  20271  f1rhm0to0ALT  20272  isabvd  20420  issrng  20450  lmodvsmmulgdi  20499  mptscmfsupp0  20529  lvecinv  20718  lspdisj2  20732  lspfixed  20733  lspexch  20734  sralem  20782  sralemOLD  20783  srasca  20790  srascaOLD  20791  sravsca  20792  sravscaOLD  20793  sraip  20794  znval  21078  psgndiflemB  21144  isphl  21172  assamulgscmlem2  21445  mplval  21539  opsrval  21592  cply1mul  21809  gsummoncoe1  21819  evl1fval  21838  scmate  22003  scmatscm  22006  mdetdiagid  22093  mdetunilem7  22111  mdetuni0  22114  gsummatr01lem3  22150  gsummatr01lem4  22151  gsummatr01  22152  slesolinvbi  22174  cpmatacl  22209  cpmatinvcl  22210  pmatcollpw2lem  22270  monmatcollpw  22272  pmatcollpwfi  22275  mp2pm2mplem4  22302  pm2mp  22318  cpmadugsumlemF  22369  cpmadugsumfi  22370  cpmadumatpoly  22376  cayhamlem4  22381  cayleyhamilton0  22382  cayleyhamiltonALT  22384  indistopon  22495  0ntr  22566  pnrmopn  22838  reftr  23009  kgenval  23030  pt1hmeo  23301  fmval  23438  fmf  23440  istmd  23569  istgp  23572  tsmsval2  23625  isxmet2d  23824  xpsxmetlem  23876  xpsmet  23879  blfvalps  23880  tmsval  23980  isnlm  24183  nmoleub  24239  idnghm  24251  blssioo  24302  blcvx  24305  icccvx  24457  pcorevlem  24533  isclm  24571  caufval  24783  iscms  24853  mbfsup  25172  i1f1  25198  dvexp3  25486  rolle  25498  dvivth  25518  deg1add  25612  0dgr  25750  coefv0  25753  elqaalem2  25824  dvradcnv  25924  abelthlem8  25942  efper  25980  logtayl  26159  abscxpbnd  26250  relogbcxpb  26281  logbgcd1irr  26288  dcubic2  26338  rlimcnp2  26460  cvxcl  26478  zetacvg  26508  lgamgulmlem2  26523  vmaval  26606  chtub  26704  logexprlim  26717  dchrsum2  26760  sumdchr2  26762  bposlem2  26777  lgsdir  26824  lgsne0  26827  lgsdirnn0  26836  lgsdinn0  26837  lgsquadlem2  26873  2lgslem3a  26888  2lgslem3b  26889  2lgslem3c  26890  2lgslem3d  26891  2lgslem3a1  26892  2lgslem3b1  26893  2lgslem3c1  26894  2lgslem3d1  26895  2sqn0  26926  dchrvmasum2if  26989  dchrvmasumiflem1  26993  rpvmasum2  27004  pntpbnd1  27078  ostth2lem4  27128  trgcgrg  27755  tgcgr4  27771  ax5seglem1  28175  ax5seglem2  28176  ax5seglem5  28180  usgr1vr  28501  cplgr2vpr  28679  cplgr3v  28681  cusgrrusgr  28827  wlklenvm1  28868  wlk0prc  28900  wlksoneq1eq2  28910  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem6  29058  crctcshlem4  29063  crctcsh  29067  wlkiswwlks1  29110  wwlksnext  29136  wwlksnextbi  29137  wwlksnextwrd  29140  midwwlks2s3  29195  clwlkclwwlklem2fv1  29237  clwlkclwwlklem2a4  29239  clwlkclwwlklem3  29243  clwwisshclwws  29257  erclwwlkeqlen  29261  clwwlkinwwlk  29282  clwwlkn2  29286  clwwlkf  29289  clwwlkf1  29291  eleclclwwlknlem2  29303  erclwwlkneqlen  29310  umgrhashecclwwlk  29320  eucrctshift  29485  eucrct2eupth  29487  fusgr2wsp2nb  29576  grpoidinvlem2  29745  vcz  29815  nvz  29909  lnon0  30038  ipasslem2  30072  htthlem  30157  hvpncan  30279  hiidge0  30338  normgt0  30367  hsn0elch  30488  shsel3  30555  spansneleq  30810  normcan  30816  h1datomi  30821  fh1  30858  spansncvi  30892  5oalem1  30894  5oalem3  30896  5oalem5  30898  3oalem2  30903  pjdsi  30952  kbpj  31196  0hmop  31223  0lnfn  31225  adj0  31234  nlelshi  31300  branmfn  31345  opsqrlem1  31380  hst1h  31467  mdsl0  31550  superpos  31594  sumdmdlem  31658  cdj3lem1  31674  f1od2  31933  xrpxdivcld  32088  xrge0npcan  32182  resvid2  32430  resvval2  32431  qsdrng  32599  esumsnf  33050  esummulc1  33067  measxun2  33196  omsmeas  33310  sibfof  33327  probun  33406  signstfvn  33568  bnj517  33884  pthhashvtx  34106  ex-sategoelel  34400  mrsubfval  34487  msrval  34517  dfrdg2  34755  bj-prmoore  35984  bj-bary1lem1  36180  rdgeqoa  36239  finxpreclem2  36259  finxpreclem3  36262  matunitlindflem1  36472  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem5  36481  poimirlem6  36482  poimirlem7  36483  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem14  36490  poimirlem15  36491  poimirlem17  36493  poimirlem20  36496  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  mblfinlem2  36514  mblfinlem3  36515  ismblfin  36517  mbfposadd  36523  itg2addnclem  36527  itg2addnclem3  36529  itg2addnc  36530  ftc1anclem8  36556  areacirc  36569  ismtyval  36656  ismrer1  36694  grposnOLD  36738  rabeq12f  37013  csbeq12  37014  iuneq12f  37019  lsatcv1  37906  glbconN  38235  glbconNOLD  38236  atltcvr  38294  3dim2  38327  islln2a  38376  2at0mat0  38384  islpln2a  38407  islvol2aN  38451  pmodlem2  38706  pmapjat1  38712  pcl0bN  38782  osumclN  38826  pexmidALTN  38837  lhp2at0nle  38894  4atexlemunv  38925  cdleme18b  39151  cdleme31sn1  39240  cdleme31sde  39244  cdleme31sn2  39248  ltrniotavalbN  39443  trljco  39599  cdlemh  39676  cdlemk40t  39777  cdlemk40f  39778  cdleml9  39843  dihmeetlem3N  40164  dochkrshp  40245  dihprrn  40285  dihjat1  40288  dvh3dim  40305  dochkrsm  40317  dochexmid  40327  lcfl7lem  40358  lcfl9a  40364  lclkrlem1  40365  mapdspex  40527  mapdindp2  40580  mapdh6dN  40598  hdmap1l6d  40672  hdmap11lem2  40701  hdmap14lem4a  40730  hdmapip0  40774  hlhilset  40793  nnadd1com  41178  sn-negex12  41285  prjspner1  41364  0prjspnrel  41365  jm2.26a  41724  onov0suclim  42009  oe0suclim  42012  cantnfresb  42059  onmcl  42066  omcl2  42068  tfsconcatun  42072  naddwordnexlem4  42137  mnringmulrcld  42972  radcnvrat  43058  sumsnd  43695  icccncfext  44589  fperdvper  44621  dvcosax  44628  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  volioc  44674  itgiccshift  44682  stoweidlem34  44736  dirkercncflem2  44806  fourierdlem32  44841  fourierdlem41  44850  fourierdlem48  44856  fourierdlem64  44872  fourierdlem73  44881  fourierdlem79  44887  fourierdlem82  44890  fourierdlem97  44905  fourierdlem101  44909  fourierdlem109  44917  fourierdlem111  44919  fouriersw  44933  elaa2  44936  etransclem24  44960  etransclem25  44961  etransclem46  44982  nnfoctbdjlem  45157  ismeannd  45169  smfpimltxr  45449  smfpimgtxr  45482  ndfatafv2undef  45906  fzopredsuc  46017  prproropf1olem3  46159  prproropf1olem4  46160  fmtnorec2lem  46196  2pwp1prmfmtno  46244  sfprmdvdsmersenne  46257  sgprmdvdsmersenne  46258  lighneallem2  46260  lighneallem3  46261  dfodd6  46291  dfeven4  46292  m1expevenALTV  46301  isomushgr  46480  isomuspgrlem2d  46485  clintopval  46600  lmod0rng  46628  zlidlring  46779  2zrngagrp  46794  rngcval  46813  ringcval  46859  dmmpossx2  46965  zlmodzxzscm  46986  zlmodzxzadd  46987  domnmsuppn0  46998  rmsuppss  46999  scmsuppss  47001  ply1mulgsumlem4  47023  ldepsprlem  47106  lincresunit2  47112  m1modmmod  47160  nn0sumshdiglemB  47259  2arymptfv  47289  ackval42  47335  affinecomb1  47341  itschlc0yqe  47399  itsclquadb  47415  2itscp  47420  0setrec  47702