Theorem syl6eqr 2190

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6eqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
syl6eqr	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2143	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eq 2188	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  3eqtr4g  2197  rabxmdc  3394  relop  4689  csbcnvg  4723  dfiun3g  4796  dfiin3g  4797  resima2  4853  relcnvfld  5072  uniabio  5098  fntpg  5179  dffn5im  5467  dfimafn2  5471  fncnvima2  5541  fmptcof  5587  fcoconst  5591  fnasrng  5600  ffnov  5875  fnovim  5879  fnrnov  5916  foov  5917  funimassov  5920  ovelimab  5921  ofc12  6002  caofinvl  6004  dftpos3  6159  tfr0dm  6219  rdgisucinc  6282  oasuc  6360  ecinxp  6504  phplem1  6746  exmidpw  6802  unfiin  6814  fidcenumlemr  6843  0ct  6992  ctmlemr  6993  exmidaclem  7064  indpi  7157  nqnq0pi  7253  nq0m0r  7271  addnqpr1  7377  recexgt0sr  7588  suplocsrlempr  7622  recidpipr  7671  recidpirq  7673  axrnegex  7694  nntopi  7709  cnref1o  9447  fztp  9865  fseq1m1p1  9882  frecuzrdgrrn  10188  frecuzrdgsuc  10194  frecuzrdgsuctlem  10203  seq3val  10238  seqvalcd  10239  fser0const  10296  mulexpzap  10340  expaddzap  10344  bcp1m1  10518  cjexp  10672  rexuz3  10769  bdtri  11018  climconst  11066  sumfct  11150  zsumdc  11160  fsum3  11163  sum0  11164  fsumcnv  11213  mertenslem2  11312  ef0lem  11373  efzval  11396  efival  11446  sinbnd  11466  cosbnd  11467  eucalgval  11742  eucalginv  11744  eucalglt  11745  eucalgcvga  11746  eucalg  11747  sqpweven  11860  2sqpwodd  11861  dfphi2  11903  phimullem  11908  ennnfonelemhdmp1  11929  ennnfonelemkh  11932  ressid2  12028  ressval2  12029  topnvalg  12142  istps  12209  cldval  12278  ntrfval  12279  clsfval  12280  neifval  12319  restbasg  12347  tgrest  12348  txval  12434  upxp  12451  uptx  12453  txrest  12455  lmcn2  12459  cnmpt2t  12472  cnmpt2res  12476  imasnopn  12478  psmetxrge0  12511  xmetge0  12544  isxms  12630  isms  12632  bdxmet  12680  qtopbasss  12700  cnblcld  12714  negfcncf  12768  dvfvalap  12829  eldvap  12830  dvidlemap  12839  dvexp2  12855  dvrecap  12856  dveflem  12865  sin0pilem1  12872  ptolemy  12915  coskpi  12939  nninfsellemqall  13221