Theorem sylan9eqr 2851

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786

This theorem is referenced by:  sbcied2  3739  csbied2  3840  opthhausdorff0  5292  fun2ssres  6261  fcoi1  6412  fcoi2  6413  funssfv  6551  fvtp1  6815  nvof1o  6893  onuninsuci  7402  ot1stg  7550  ot2ndg  7551  el2xptp0  7583  mpomptsx  7609  dmmpossx  7611  fmpox  7612  2ndconst  7643  mpoxopoveq  7727  wfrlem10  7807  rdgeq12  7892  rdgsucmptnf  7908  frsucmptn  7917  oev2  7990  oesuclem  7992  oawordeulem  8021  om00  8042  omass  8047  omeulem1  8049  oeoa  8064  oeoe  8066  nnmass  8091  oaabs2  8113  omabs  8115  mapsnend  8426  omxpenlem  8455  sbthlem4  8467  sbthlem6  8469  fodomr  8505  ssenen  8528  fi0  8720  cantnfp1  8979  cnfcomlem  8997  cardaleph  9350  cflim2  9520  axdc4lem  9712  fpwwe2lem12  9898  fpwwe2lem13  9899  rankcf  10034  inatsk  10035  ltrnq  10236  addclprlem1  10273  mulclprlem  10276  1idpr  10286  prlem936  10304  reclem3pr  10306  mulcmpblnrlem  10327  recexsrlem  10360  map2psrpr  10367  addid0  10896  subdivcomb2  11173  nnnn0addcl  11764  zindd  11921  qaddcl  12203  qmulcl  12205  qreccl  12207  xaddnemnf  12468  xaddnepnf  12469  xaddcom  12472  xnegdi  12480  xaddass  12481  xpncan  12483  xleadd1a  12485  xlt2add  12492  rexmul  12503  xmulgt0  12515  xmulge0  12516  xmulasslem3  12518  xlemul1a  12520  xadddilem  12526  xadddi2  12529  modmuladd  13119  modm1p1mod0  13128  modfzo0difsn  13149  seqf1olem2  13248  expp1  13274  expneg  13275  expcllem  13278  mulexp  13306  expmul  13312  sqoddm1div8  13442  bcpasc  13519  hashrabsn01  13570  fseq1hash  13573  hashinfxadd  13582  hashfzo  13626  fnfz0hash  13640  ffzo0hash  13643  hashf1lem1  13649  hashge2el2dif  13672  hashdifsnp1  13688  lsw0  13751  ccatval1  13763  ccatval2  13764  swrdval  13829  reuccatpfxs1  13933  splval  13937  repswswrd  13970  2cshwcshw  14011  s4dom  14105  wrdlen2i  14128  shftfn  14254  reim0b  14300  cjexp  14331  sqeqd  14347  fsumser  14908  sumsnf  14920  binomlem  15005  expcnv  15040  prodsn  15137  prodsnf  15139  bpolylem  15223  bpoly2  15232  bpoly3  15233  ef0lem  15253  dvdsnegb  15448  mod2eq1n2dvds  15517  m1expe  15546  m1expo  15547  m1exp1  15548  flodddiv4  15585  sadadd2lem2  15620  gcdabs  15698  bezoutr1  15730  dvdslcm  15759  lcmeq0  15761  lcmcl  15762  lcmabs  15766  lcmgcdlem  15767  lcmdvds  15769  lcmf0val  15783  lcmftp  15797  lcmfunsnlem2  15801  mulgcddvds  15816  divgcdcoprmex  15827  pcge0  16015  pcadd  16042  pcmpt2  16046  prmreclem4  16072  ramval  16161  ramcl  16182  fvprmselelfz  16197  fvprmselgcd1  16198  ressid2  16369  ressval2  16370  mndind  17793  frmdval  17815  mgm2nsgrplem3  17834  mulgfval  17971  mulgfvalALT  17972  mulgnn0subcl  17984  mulgnn0z  17996  isga  18150  symgval  18226  symgextfve  18266  symgfixf1  18284  f1omvdco2  18295  psgnsn  18367  odid  18385  gexid  18424  frgpuptinv  18612  frgpup2  18617  dprdsn  18863  srgmulgass  18959  srgpcomp  18960  srgbinomlem4  18971  ringinvnzdiv  19021  f1ghm0to0  19170  f1rhm0to0OLD  19171  f1rhm0to0ALT  19172  isabvd  19269  issrng  19299  lmodvsmmulgdi  19347  mptscmfsupp0  19377  lvecinv  19563  lspdisj2  19577  lspfixed  19578  lspexch  19579  sralem  19627  srasca  19631  sravsca  19632  sraip  19633  assamulgscmlem2  19805  mplval  19884  opsrval  19930  cply1mul  20133  gsummoncoe1  20143  evl1fval  20161  znval  20352  psgndiflemB  20414  isphl  20442  scmate  20791  scmatscm  20794  mdetdiagid  20881  mdetunilem7  20899  mdetuni0  20902  gsummatr01lem3  20938  gsummatr01lem4  20939  gsummatr01  20940  slesolinvbi  20962  cpmatacl  20996  cpmatinvcl  20997  pmatcollpw2lem  21057  monmatcollpw  21059  pmatcollpwfi  21062  mp2pm2mplem4  21089  pm2mp  21105  cpmadugsumlemF  21156  cpmadugsumfi  21157  cpmadumatpoly  21163  cayhamlem4  21168  cayleyhamilton0  21169  cayleyhamiltonALT  21171  indistopon  21281  0ntr  21351  pnrmopn  21623  reftr  21794  kgenval  21815  pt1hmeo  22086  fmval  22223  fmf  22225  istmd  22354  istgp  22357  tsmsval2  22409  isxmet2d  22608  xpsxmetlem  22660  xpsmet  22663  blfvalps  22664  tmsval  22762  isnlm  22955  nmoleub  23011  idnghm  23023  blssioo  23074  blcvx  23077  icccvx  23225  pcorevlem  23301  isclm  23339  caufval  23549  iscms  23619  mbfsup  23936  i1f1  23962  dvexp3  24246  rolle  24258  dvivth  24278  deg1add  24368  0dgr  24506  coefv0  24509  elqaalem2  24580  dvradcnv  24680  abelthlem8  24698  efper  24736  logtayl  24912  abscxpbnd  25003  relogbcxpb  25034  logbgcd1irr  25041  dcubic2  25091  rlimcnp2  25214  cvxcl  25232  zetacvg  25262  lgamgulmlem2  25277  vmaval  25360  chtub  25458  logexprlim  25471  dchrsum2  25514  sumdchr2  25516  bposlem2  25531  lgsdir  25578  lgsne0  25581  lgsdirnn0  25590  lgsdinn0  25591  lgsquadlem2  25627  2lgslem3a  25642  2lgslem3b  25643  2lgslem3c  25644  2lgslem3d  25645  2lgslem3a1  25646  2lgslem3b1  25647  2lgslem3c1  25648  2lgslem3d1  25649  2sqn0  25680  dchrvmasum2if  25743  dchrvmasumiflem1  25747  rpvmasum2  25758  pntpbnd1  25832  ostth2lem4  25882  trgcgrg  25971  ax5seglem1  26385  ax5seglem2  26386  ax5seglem5  26390  usgr1vr  26708  cplgr2vpr  26886  cplgr3v  26888  cusgrrusgr  27034  wlklenvm1  27074  wlk0prc  27106  wlksoneq1eq2  27116  crctcshwlkn0lem4  27266  crctcshwlkn0lem5  27267  crctcshwlkn0lem6  27268  crctcshlem4  27273  crctcsh  27277  wlkiswwlks1  27320  wwlksnextbi  27347  wwlksnextwrd  27350  midwwlks2s3  27406  clwlkclwwlklem2fv1  27448  clwlkclwwlklem2a4  27450  clwlkclwwlklem3  27454  clwwisshclwws  27468  erclwwlkeqlen  27472  clwwlkinwwlk  27493  clwwlkn2  27497  clwwlkf  27501  clwwlkf1  27503  eleclclwwlknlem2  27515  erclwwlkneqlen  27522  umgrhashecclwwlk  27532  eucrctshift  27698  eucrct2eupthOLD  27701  eucrct2eupth  27702  fusgr2wsp2nb  27793  grpoidinvlem2  27961  vcz  28031  nvz  28125  lnon0  28254  ipasslem2  28288  htthlem  28373  hvpncan  28495  hiidge0  28554  normgt0  28583  hsn0elch  28704  shsel3  28771  spansneleq  29026  normcan  29032  h1datomi  29037  fh1  29074  spansncvi  29108  5oalem1  29110  5oalem3  29112  5oalem5  29114  3oalem2  29119  pjdsi  29168  kbpj  29412  0hmop  29439  0lnfn  29441  adj0  29450  nlelshi  29516  branmfn  29561  opsqrlem1  29596  hst1h  29683  mdsl0  29766  superpos  29810  sumdmdlem  29874  cdj3lem1  29890  f1od2  30118  xrpxdivcld  30266  xrge0npcan  30325  resvid2  30510  resvval2  30511  esumsnf  30896  esummulc1  30913  measxun2  31042  omsmeas  31154  sibfof  31171  probun  31250  bnj517  31729  pthhashvtx  31938  sategoelelxmpl  32229  mrsubfval  32308  msrval  32338  dfrdg2  32594  bj-bary1lem1  34075  rdgeqoa  34128  finxpreclem2  34148  finxpreclem3  34151  matunitlindflem1  34365  poimirlem1  34370  poimirlem2  34371  poimirlem3  34372  poimirlem4  34373  poimirlem5  34374  poimirlem6  34375  poimirlem7  34376  poimirlem10  34379  poimirlem11  34380  poimirlem12  34381  poimirlem14  34383  poimirlem15  34384  poimirlem17  34386  poimirlem20  34389  poimirlem22  34391  poimirlem23  34392  poimirlem24  34393  poimirlem25  34394  poimirlem26  34395  poimirlem27  34396  mblfinlem2  34407  mblfinlem3  34408  ismblfin  34410  mbfposadd  34416  itg2addnclem  34420  itg2addnclem3  34422  itg2addnc  34423  ftc1anclem8  34451  areacirc  34464  ismtyval  34556  ismrer1  34594  grposnOLD  34638  rabeq12f  34915  csbeq12  34916  iuneq12f  34921  lsatcv1  35665  glbconN  35994  atltcvr  36052  3dim2  36085  islln2a  36134  2at0mat0  36142  islpln2a  36165  islvol2aN  36209  pmodlem2  36464  pmapjat1  36470  pcl0bN  36540  osumclN  36584  pexmidALTN  36595  lhp2at0nle  36652  4atexlemunv  36683  cdleme18b  36909  cdleme31sn1  36998  cdleme31sde  37002  cdleme31sn2  37006  ltrniotavalbN  37201  trljco  37357  cdlemh  37434  cdlemk40t  37535  cdlemk40f  37536  cdleml9  37601  dihmeetlem3N  37922  dochkrshp  38003  dihprrn  38043  dihjat1  38046  dvh3dim  38063  dochkrsm  38075  dochexmid  38085  lcfl7lem  38116  lcfl9a  38122  lclkrlem1  38123  mapdspex  38285  mapdindp2  38338  mapdh6dN  38356  hdmap1l6d  38430  hdmap11lem2  38459  hdmap14lem4a  38488  hdmapip0  38532  hlhilset  38551  nnadd1com  38635  0prjspnrel  38716  jm2.26a  39033  radcnvrat  40136  sumsnd  40774  icccncfext  41665  fperdvper  41698  dvcosax  41706  ioodvbdlimc1lem1  41711  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  volioc  41752  itgiccshift  41760  stoweidlem34  41815  dirkercncflem2  41885  fourierdlem32  41920  fourierdlem41  41929  fourierdlem48  41935  fourierdlem64  41951  fourierdlem73  41960  fourierdlem79  41966  fourierdlem82  41969  fourierdlem97  41984  fourierdlem101  41988  fourierdlem109  41996  fourierdlem111  41998  fouriersw  42012  elaa2  42015  etransclem24  42039  etransclem25  42040  etransclem46  42061  nnfoctbdjlem  42233  ismeannd  42245  ndfatafv2undef  42881  fzopredsuc  42993  prproropf1olem3  43103  prproropf1olem4  43104  fmtnorec2lem  43140  2pwp1prmfmtno  43188  sfprmdvdsmersenne  43204  sgprmdvdsmersenne  43205  lighneallem2  43207  lighneallem3  43208  dfodd6  43238  dfeven4  43239  m1expevenALTV  43248  isomushgr  43427  isomuspgrlem2d  43432  clintopval  43543  lmod0rng  43571  zlidlring  43631  2zrngagrp  43646  rngcval  43665  ringcval  43711  dmmpossx2  43817  zlmodzxzscm  43837  zlmodzxzadd  43838  domnmsuppn0  43851  rmsuppss  43852  scmsuppss  43854  ply1mulgsumlem4  43877  ldepsprlem  43961  lincresunit2  43967  m1modmmod  44016  nn0sumshdiglemB  44115  affinecomb1  44124  itschlc0yqe  44182  itsclquadb  44198  2itscp  44203  0setrec  44240