Theorem sylan9eqr 2822

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  sbcied2  3790  csbied2  3891  opthhausdorff0  5503  fun2ssres  6585  fcoi1  6756  fcoi2  6757  funssfv  6906  fvtp1  7197  nvof1o  7284  onuninsuci  7838  ot1stg  8002  ot2ndg  8003  el2xptp0  8035  mpomptsx  8063  dmmpossx  8065  fmpox  8066  2ndconst  8098  offsplitfpar  8116  mpoxopoveq  8217  rdgeq12  8402  rdgsucmptnf  8418  frsucmptn  8428  oev2  8510  oesuclem  8512  oawordeulem  8541  om00  8562  omass  8567  omeulem1  8569  oeoa  8585  oeoe  8587  nnmass  8612  oaabs2  8637  omabs  8639  mapsnend  9036  omxpenlem  9069  sbthlem4  9081  sbthlem6  9083  fodomr  9119  ssenen  9142  fodomfir  9290  fi0  9383  cantnfp1  9653  cnfcomlem  9671  ttrclselem2  9698  cardaleph  10085  cflim2  10258  axdc4lem  10450  fpwwe2lem11  10637  fpwwe2lem12  10638  rankcf  10773  inatsk  10774  ltrnq  10975  addclprlem1  11012  mulclprlem  11015  1idpr  11025  prlem936  11043  reclem3pr  11045  mulcmpblnrlem  11066  recexsrlem  11099  map2psrpr  11106  addid0  11644  subdivcomb2  11922  nnadd1com  12270  nnnn0addcl  12545  zindd  12709  qaddcl  13001  qmulcl  13003  qreccl  13005  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  xaddass  13287  xpncan  13289  xleadd1a  13291  xlt2add  13298  rexmul  13309  xmulgt0  13321  xmulge0  13322  xmulasslem3  13324  xlemul1a  13326  xadddilem  13332  xadddi2  13335  modmuladd  13963  modm1p1mod0  13972  modfzo0difsn  13993  seqf1olem2  14092  expp1  14118  expneg  14119  expcllem  14122  mulexp  14151  expmul  14157  sqoddm1div8  14293  bcpasc  14371  hashrabsn01  14423  fseq1hash  14426  hashinfxadd  14435  hashfzo  14480  fnfz0hash  14497  ffzo0hash  14500  hashf1lem1  14506  hashge2el2dif  14531  hash3tpexb  14545  hashdifsnp1  14557  lsw0  14616  ccatval1  14628  ccatval2  14629  swrdval  14697  ccatopth  14771  reuccatpfxs1  14802  splval  14806  repswswrd  14841  2cshwcshw  14882  s4dom  14976  wrdlen2i  14999  shftfn  15130  reim0b  15190  cjexp  15221  sqeqd  15237  fsumser  15800  sumsnf  15813  binomlem  15902  expcnv  15937  prodsn  16035  prodsnf  16037  bpolylem  16120  bpoly2  16129  bpoly3  16130  ef0lem  16150  dvdsnegb  16349  mod2eq1n2dvds  16423  m1expe  16450  m1expo  16451  m1exp1  16452  flodddiv4  16491  sadadd2lem2  16526  bezoutr1  16645  dvdslcm  16674  lcmeq0  16676  lcmcl  16677  lcmabs  16681  lcmgcdlem  16682  lcmdvds  16684  lcmf0val  16698  lcmftp  16712  lcmfunsnlem2  16716  mulgcddvds  16731  divgcdcoprmex  16742  pcge0  16940  pcadd  16967  pcmpt2  16971  prmreclem4  16997  ramval  17086  ramcl  17107  fvprmselelfz  17122  fvprmselgcd1  17123  ressid2  17312  ressval2  17313  mndind  18911  frmdval  18934  efmnd  18953  smndex1igid  18989  smndex1igidOLD  18990  smndex1n0mnd  18998  mgm2nsgrplem3  19006  mulgfval  19159  mulgfvalALT  19160  mulgnn0subcl  19177  mulgnn0z  19191  cycsubm  19297  f1ghm0to0  19339  isga  19385  symgextfve  19513  symgfixf1  19531  f1omvdco2  19542  psgnsn  19614  odid  19632  gexid  19675  efgsval2  19827  frgpuptinv  19865  frgpup2  19870  dprdsn  20132  srgmulgass  20323  srgpcomp  20324  srgbinomlem4  20335  ringinvnzdiv  20410  rngcval  20747  ringcval  20776  isabvd  20945  issrng  20977  lmodvsmmulgdi  21048  mptscmfsupp0  21078  lvecinv  21267  lspdisj2  21281  lspfixed  21282  lspexch  21283  sralem  21327  srasca  21331  sravsca  21332  sraip  21333  znval  21715  psgndiflemB  21780  isphl  21808  assamulgscmlem2  22080  mplval  22168  opsrval  22227  psdmvr  22362  cply1mul  22486  gsummoncoe1  22498  evl1fval  22518  scmate  22697  scmatscm  22700  mdetdiagid  22787  mdetunilem7  22805  mdetuni0  22808  gsummatr01lem3  22844  gsummatr01lem4  22845  gsummatr01  22846  slesolinvbi  22868  cpmatacl  22903  cpmatinvcl  22904  pmatcollpw2lem  22964  monmatcollpw  22966  pmatcollpwfi  22969  mp2pm2mplem4  22996  pm2mp  23012  cpmadugsumlemF  23063  cpmadugsumfi  23064  cpmadumatpoly  23070  cayhamlem4  23075  cayleyhamilton0  23076  cayleyhamiltonALT  23078  indistopon  23188  0ntr  23258  pnrmopn  23530  reftr  23702  kgenval  23723  pt1hmeo  23994  fmval  24131  fmf  24133  istmd  24262  istgp  24265  tsmsval2  24318  isxmet2d  24515  xpsxmetlem  24567  xpsmet  24570  blfvalps  24571  tmsval  24669  isnlm  24863  nmoleub  24919  idnghm  24931  blssioo  24983  blcvx  24986  icccvx  25140  pcorevlem  25216  isclm  25254  caufval  25465  iscms  25535  mbfsup  25854  i1f1  25880  dvexp3  26168  rolle  26180  dvivth  26200  deg1add  26291  0dgr  26433  coefv0  26436  elqaalem2  26512  dvradcnv  26615  abelthlem8  26633  efper  26675  logtayl  26856  abscxpbnd  26949  relogbcxpb  26983  logbgcd1irr  26990  dcubic2  27040  rlimcnp2  27162  cvxcl  27180  zetacvg  27210  lgamgulmlem2  27225  vmaval  27308  chtub  27407  logexprlim  27420  dchrsum2  27463  sumdchr2  27465  bposlem2  27480  lgsdir  27527  lgsne0  27530  lgsdirnn0  27539  lgsdinn0  27540  lgsquadlem2  27576  2lgslem3a  27591  2lgslem3b  27592  2lgslem3c  27593  2lgslem3d  27594  2lgslem3a1  27595  2lgslem3b1  27596  2lgslem3c1  27597  2lgslem3d1  27598  2sqn0  27629  dchrvmasum2if  27692  dchrvmasumiflem1  27696  rpvmasum2  27707  pntpbnd1  27781  ostth2lem4  27831  expsp1  28653  trgcgrg  28815  tgcgr4  28831  ax5seglem1  29309  ax5seglem2  29310  ax5seglem5  29314  usgr1vr  29639  cplgr2vpr  29817  cplgr3v  29819  cusgrrusgr  29965  wlklenvm1  30005  wlk0prc  30036  wlksoneq1eq2  30046  pthhashvtx  30118  crctcshwlkn0lem4  30205  crctcshwlkn0lem5  30206  crctcshwlkn0lem6  30207  crctcshlem4  30212  crctcsh  30216  wlkiswwlks1  30259  wwlksnext  30285  wwlksnextbi  30286  wwlksnextwrd  30289  midwwlks2s3  30344  clwlkclwwlklem2fv1  30389  clwlkclwwlklem2a4  30391  clwlkclwwlklem3  30395  clwwisshclwws  30409  erclwwlkeqlen  30413  clwwlkinwwlk  30434  clwwlkn2  30438  clwwlkf  30441  clwwlkf1  30443  eleclclwwlknlem2  30455  erclwwlkneqlen  30462  umgrhashecclwwlk  30472  eucrctshift  30641  eucrct2eupth  30643  fusgr2wsp2nb  30732  grpoidinvlem2  30904  vcz  30974  nvz  31068  lnon0  31197  ipasslem2  31231  htthlem  31316  hvpncan  31438  hiidge0  31497  normgt0  31526  hsn0elch  31647  shsel3  31714  spansneleq  31969  normcan  31975  h1datomi  31980  fh1  32017  spansncvi  32051  5oalem1  32053  5oalem3  32055  5oalem5  32057  3oalem2  32062  pjdsi  32111  kbpj  32355  0hmop  32382  0lnfn  32384  adj0  32393  nlelshi  32459  branmfn  32504  opsqrlem1  32539  hst1h  32626  mdsl0  32709  superpos  32753  sumdmdlem  32817  cdj3lem1  32833  f1od2  33110  xrpxdivcld  33300  xrge0npcan  33380  elrgspnlem2  33603  rlocf1  33634  resvid2  33690  resvval2  33691  qsdrng  33819  r1pquslmic  33940  0mplrim  33944  selvply1rhmlemb  33949  selvply1rhmlem2  33951  selvply1rhmlem4  33953  mplvrpmmhm  33976  mplvrpmrhm  33977  esplyfval0  33994  esplyfvaln  34004  vietalem  34009  rtelextdg2lem  34156  esumsnf  34494  esummulc1  34511  measxun2  34641  omsmeas  34754  sibfof  34771  probun  34850  signstfvn  34997  bnj517  35314  ex-sategoelel  35926  mrsubfval  36013  msrval  36043  dfrdg2  36298  itgeq12i  36751  bj-prmoore  37790  bj-bary1lem1  37988  rdgeqoa  38049  finxpreclem2  38069  finxpreclem3  38072  matunitlindflem1  38300  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem14  38318  poimirlem15  38319  poimirlem17  38321  poimirlem20  38324  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  mblfinlem2  38342  mblfinlem3  38343  ismblfin  38345  mbfposadd  38351  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  ftc1anclem8  38384  areacirc  38397  ismtyval  38484  ismrer1  38522  grposnOLD  38566  rabeq12f  38839  csbeq12  38840  iuneq12f  38845  lsatcv1  39855  glbconN  40184  atltcvr  40242  3dim2  40275  islln2a  40324  2at0mat0  40332  islpln2a  40355  islvol2aN  40399  pmodlem2  40654  pmapjat1  40660  pcl0bN  40730  osumclN  40774  pexmidALTN  40785  lhp2at0nle  40842  4atexlemunv  40873  cdleme18b  41099  cdleme31sn1  41188  cdleme31sde  41192  cdleme31sn2  41196  ltrniotavalbN  41391  trljco  41547  cdlemh  41624  cdlemk40t  41725  cdlemk40f  41726  cdleml9  41791  dihmeetlem3N  42112  dochkrshp  42193  dihprrn  42233  dihjat1  42236  dvh3dim  42253  dochkrsm  42265  dochexmid  42275  lcfl7lem  42306  lcfl9a  42312  lclkrlem1  42313  mapdspex  42475  mapdindp2  42528  mapdh6dN  42546  hdmap1l6d  42620  hdmap11lem2  42649  hdmap14lem4a  42678  hdmapip0  42722  hlhilset  42741  mulgt0b2d  43285  fiabv  43337  prjspner1  43391  0prjspnrel  43392  jm2.26a  43760  onov0suclim  44034  oe0suclim  44037  cantnfresb  44084  onmcl  44091  omcl2  44093  tfsconcatun  44097  naddwordnexlem4  44161  mnringmulrcld  44985  radcnvrat  45057  sumsnd  45779  icccncfext  46634  fperdvper  46666  dvcosax  46673  ioodvbdlimc1lem1  46678  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  volioc  46719  itgiccshift  46727  stoweidlem34  46781  dirkercncflem2  46851  fourierdlem32  46886  fourierdlem41  46895  fourierdlem48  46901  fourierdlem64  46917  fourierdlem73  46926  fourierdlem79  46932  fourierdlem82  46935  fourierdlem97  46950  fourierdlem101  46954  fourierdlem109  46962  fourierdlem111  46964  fouriersw  46978  elaa2  46981  etransclem24  47005  etransclem25  47006  etransclem46  47027  nnfoctbdjlem  47202  ismeannd  47214  smfpimltxr  47494  smfpimgtxr  47527  ndfatafv2undef  47982  fzopredsuc  48094  m1modmmod  48134  modlt0b  48139  prproropf1olem3  48287  prproropf1olem4  48288  fmtnorec2lem  48327  2pwp1prmfmtno  48375  sfprmdvdsmersenne  48388  sgprmdvdsmersenne  48389  lighneallem2  48391  lighneallem3  48392  ppivalnnprm  48410  ppivalnnnprmge6  48411  dfodd6  48435  dfeven4  48436  m1expevenALTV  48445  isubgredg  48664  upgrimwlklem5  48699  gricushgr  48715  stgrusgra  48757  isubgr3stgrlem8  48771  clintopval  49002  lmod0rng  49027  zlidlring  49032  2zrngagrp  49047  dmmpossx2  49150  zlmodzxzscm  49170  zlmodzxzadd  49171  domnmsuppn0  49182  rmsuppss  49183  scmsuppss  49184  ply1mulgsumlem4  49202  ldepsprlem  49285  lincresunit2  49291  nn0sumshdiglemB  49433  2arymptfv  49463  ackval42  49509  affinecomb1  49515  itschlc0yqe  49573  itsclquadb  49589  2itscp  49594  incat  50412  0setrec  50515