Theorem sylan9eqr 2666

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  sbcied2  3440  csbied2  3527  fun2ssres  5845  fcoi1  5991  fcoi2  5992  funssfv  6119  fvtp1  6365  nvof1o  6436  onuninsuci  6932  ot1stg  7073  ot2ndg  7074  el2xptp0  7103  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  2ndconst  7153  mpt2xopoveq  7232  wfrlem10  7311  rdgeq12  7396  rdgsucmptnf  7412  frsucmptn  7421  oev2  7490  oesuclem  7492  oawordeulem  7521  om00  7542  omass  7547  oeoa  7564  oeoe  7566  nnmass  7591  oaabs2  7612  omabs  7614  omxpenlem  7946  sbthlem4  7958  sbthlem6  7960  fodomr  7996  ssenen  8019  fi0  8209  cantnfp1  8461  cnfcomlem  8479  cardaleph  8795  cflim2  8968  axdc4lem  9160  fpwwe2lem12  9342  fpwwe2lem13  9343  rankcf  9478  inatsk  9479  ltrnq  9680  addclprlem1  9717  mulclprlem  9720  1idpr  9730  prlem936  9748  reclem3pr  9750  mulcmpblnrlem  9770  recexsrlem  9803  map2psrpr  9810  addid0  10329  nnnn0addcl  11200  zindd  11354  qaddcl  11680  qmulcl  11682  qreccl  11684  xaddnemnf  11941  xaddnepnf  11942  xaddcom  11945  xnegdi  11950  xaddass  11951  xpncan  11953  xleadd1a  11955  xlt2add  11962  rexmul  11973  xmulgt0  11985  xmulge0  11986  xmulasslem3  11988  xlemul1a  11990  xadddilem  11996  xadddi2  11999  modmuladd  12574  modm1p1mod0  12583  modfzo0difsn  12604  seqf1olem2  12703  expp1  12729  expneg  12730  expcllem  12733  mulexp  12761  expmul  12767  sqoddm1div8  12890  bcpasc  12970  hashrabsn01  13023  fseq1hash  13026  hashinfxadd  13035  hashfzo  13076  fnfz0hash  13087  ffzo0hash  13090  hashf1lem1  13096  hashge2el2dif  13117  brfi1indlem  13133  lsw0  13205  ccatval1  13214  ccatval2  13215  swrdval  13269  reuccats1  13332  splval  13353  repswswrd  13382  2cshwcshw  13422  s4dom  13514  wrdlen2i  13534  shftfn  13661  reim0b  13707  cjexp  13738  sqeqd  13754  fsumser  14308  sumsn  14319  binomlem  14400  expcnv  14435  prodsn  14531  prodsnf  14533  bpolylem  14618  bpoly2  14627  bpoly3  14628  ef0lem  14648  dvdsnegb  14837  mod2eq1n2dvds  14909  m1expe  14929  m1expo  14930  m1exp1  14931  flodddiv4  14975  sadadd2lem2  15010  gcdabs  15088  bezoutr1  15120  dvdslcm  15149  lcmeq0  15151  lcmcl  15152  lcmabs  15156  lcmgcdlem  15157  lcmdvds  15159  lcmf0val  15173  lcmftp  15187  lcmfunsnlem2  15191  coprmdvdsOLD  15205  mulgcddvds  15207  divgcdcoprmex  15218  pcge0  15404  pcadd  15431  pcmpt2  15435  prmreclem4  15461  ramval  15550  ramcl  15571  fvprmselelfz  15586  fvprmselgcd1  15587  ressid2  15755  ressval2  15756  mrcmndind  17189  frmdval  17211  mgm2nsgrplem3  17230  mulgfval  17365  mulgnn0subcl  17377  mulgnn0z  17390  isga  17547  symgval  17622  symgextfve  17662  symgfixf1  17680  f1omvdco2  17691  psgnsn  17763  odid  17780  gexid  17819  frgpuptinv  18007  frgpup2  18012  dprdsn  18258  srgmulgass  18354  srgpcomp  18355  srgbinomlem4  18366  ringinvnzdiv  18416  f1rhm0to0  18563  f1rhm0to0ALT  18564  isabvd  18643  issrng  18673  lmodvsmmulgdi  18721  mptscmfsupp0  18751  lvecinv  18934  lspdisj2  18948  lspfixed  18949  lspexch  18950  sralem  18998  srasca  19002  sravsca  19003  sraip  19004  assamulgscmlem2  19170  mplval  19249  opsrval  19295  cply1mul  19485  gsummoncoe1  19495  evl1fval  19513  znval  19702  psgndiflemB  19765  isphl  19792  scmate  20135  scmatscm  20138  mdetdiagid  20225  mdetunilem7  20243  mdetuni0  20246  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  slesolinvbi  20306  cpmatacl  20340  cpmatinvcl  20341  pmatcollpw2lem  20401  monmatcollpw  20403  pmatcollpwfi  20406  mp2pm2mplem4  20433  pm2mp  20449  cpmadugsumlemF  20500  cpmadugsumfi  20501  cpmadumatpoly  20507  cayhamlem4  20512  cayleyhamilton0  20513  cayleyhamiltonALT  20515  indistopon  20615  0ntr  20685  pnrmopn  20957  reftr  21127  kgenval  21148  pt1hmeo  21419  fmval  21557  fmf  21559  istmd  21688  istgp  21691  tsmsval2  21743  isxmet2d  21942  xpsxmetlem  21994  xpsmet  21997  blfvalps  21998  tmsval  22096  isnlm  22289  nmoleub  22345  idnghm  22357  blssioo  22406  blcvx  22409  icccvx  22557  pcorevlem  22634  isclm  22672  caufval  22881  iscms  22950  mbfsup  23237  i1f1  23263  dvexp3  23545  rolle  23557  dvivth  23577  deg1add  23667  0dgr  23805  coefv0  23808  elqaalem2  23879  dvradcnv  23979  abelthlem8  23997  efper  24035  logtayl  24206  abscxpbnd  24294  relogbcxpb  24325  dcubic2  24371  rlimcnp2  24493  cvxcl  24511  zetacvg  24541  lgamgulmlem2  24556  vmaval  24639  chtub  24737  logexprlim  24750  dchrsum2  24793  sumdchr2  24795  bposlem2  24810  lgsdir  24857  lgsne0  24860  lgsdirnn0  24869  lgsdinn0  24870  lgsquadlem2  24906  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  dchrvmasum2if  24986  dchrvmasumiflem1  24990  rpvmasum2  25001  pntpbnd1  25075  ostth2lem4  25125  trgcgrg  25210  ax5seglem1  25608  ax5seglem2  25609  ax5seglem5  25613  usgraedgprv  25905  wwlknimp  26215  wwlknextbi  26253  wwlkextwrd  26256  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem0  26316  clwwlkf  26322  clwwlkf1  26324  wwlkext2clwwlk  26331  clwwisshclww  26335  erclwwlkeqlen  26340  eleclclwwlknlem2  26346  erclwwlkneqlen  26352  usghashecclwwlk  26362  vdgr1d  26430  vdgr1b  26431  vdgr1a  26433  cusgraisrusgra  26465  rusgra0edg  26482  eupatrl  26495  usg2spot2nb  26592  grpoidinvlem2  26743  vcz  26814  nvz  26908  lnon0  27037  ipasslem2  27071  htthlem  27158  hvpncan  27280  hiidge0  27339  normgt0  27368  hsn0elch  27489  shsel3  27558  spansneleq  27813  normcan  27819  h1datomi  27824  fh1  27861  spansncvi  27895  5oalem1  27897  5oalem3  27899  5oalem5  27901  3oalem2  27906  pjdsi  27955  kbpj  28199  0hmop  28226  0lnfn  28228  adj0  28237  nlelshi  28303  branmfn  28348  opsqrlem1  28383  hst1h  28470  mdsl0  28553  superpos  28597  sumdmdlem  28661  cdj3lem1  28677  xrpxdivcld  28974  2sqn0  28977  xrge0npcan  29025  resvid2  29159  resvval2  29160  esumsnf  29453  esummulc1  29470  measxun2  29600  omsmeas  29712  sibfof  29729  probun  29808  bnj517  30209  mrsubfval  30659  msrval  30689  subdivcomb2  30865  dfrdg2  30945  bj-bary1lem1  32338  rdgeqoa  32394  finxpreclem2  32403  finxpreclem3  32406  matunitlindflem1  32575  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem14  32593  poimirlem15  32594  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  mbfposadd  32627  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem8  32662  areacirc  32675  ismtyval  32769  ismrer1  32807  grposnOLD  32851  rabeq12f  33135  csbeq12  33136  iuneq12f  33142  lsatcv1  33353  glbconN  33681  atltcvr  33739  3dim2  33772  islln2a  33821  2at0mat0  33829  islpln2a  33852  islvol2aN  33896  pmodlem2  34151  pmapjat1  34157  pcl0bN  34227  osumclN  34271  pexmidALTN  34282  lhp2at0nle  34339  4atexlemunv  34370  cdleme18b  34597  cdleme31sn1  34687  cdleme31sde  34691  cdleme31sn2  34695  ltrniotavalbN  34890  trljco  35046  cdlemh  35123  cdlemk40t  35224  cdlemk40f  35225  cdleml9  35290  dihmeetlem3N  35612  dochkrshp  35693  dihprrn  35733  dihjat1  35736  dvh3dim  35753  dochkrsm  35765  dochexmid  35775  lcfl7lem  35806  lcfl9a  35812  lclkrlem1  35813  mapdspex  35975  mapdindp2  36028  mapdh6dN  36046  hdmap1l6d  36121  hdmap11lem2  36152  hdmap14lem4a  36181  hdmapip0  36225  hlhilset  36244  jm2.26a  36585  radcnvrat  37535  sumsnd  38208  sumsnf  38636  icccncfext  38773  fperdvper  38808  dvcosax  38816  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  volioc  38864  itgiccshift  38872  stoweidlem34  38927  dirkercncflem2  38997  fourierdlem32  39032  fourierdlem41  39041  fourierdlem48  39047  fourierdlem64  39063  fourierdlem73  39072  fourierdlem79  39078  fourierdlem82  39081  fourierdlem97  39096  fourierdlem101  39100  fourierdlem109  39108  fourierdlem111  39110  fouriersw  39124  elaa2  39127  etransclem24  39151  etransclem25  39152  etransclem46  39173  nnfoctbdjlem  39348  ismeannd  39360  fzopredsuc  39946  fmtnorec2lem  39992  2pwp1prmfmtno  40042  sfprmdvdsmersenne  40058  sgprmdvdsmersenne  40059  lighneallem2  40061  lighneallem3  40062  dfodd6  40088  dfeven4  40089  m1expevenALTV  40098  usgr1vr  40481  cplgr2vpr  40655  cplgr3v  40657  cusgrrusgr  40781  1wlklenvm1  40826  1wlk0prc  40862  wlksoneq1eq2  40872  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  crctcshlem4  41023  crctcsh  41027  1wlkiswwlks1  41064  wwlksnextbi  41100  wwlksnextwrd  41103  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2a4  41206  clwlkclwwlklem3  41210  clwwlksn2  41217  clwwlksf  41222  clwwlksf1  41224  wwlksext2clwwlk  41231  clwwisshclwws  41235  erclwwlkseqlen  41240  eleclclwwlksnlem2  41246  erclwwlksneqlen  41252  umgrhashecclwwlk  41262  eucrctshift  41411  eucrct2eupth  41413  fusgr2wsp2nb  41498  av-extwwlkfablem2  41510  clintopval  41630  lmod0rng  41658  2zrngagrp  41733  rngcval  41754  ringcval  41800  dmmpt2ssx2  41908  zlmodzxzscm  41928  zlmodzxzadd  41929  domnmsuppn0  41944  rmsuppss  41945  scmsuppss  41947  ply1mulgsumlem4  41971  ldepsprlem  42055  lincresunit2  42061  m1modmmod  42110  nn0sumshdiglemB  42212  0setrec  42246