Theorem syl6eqr 2150

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 2104	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eq 2148	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  3eqtr4g  2157  rabxmdc  3341  relop  4627  csbcnvg  4661  dfiun3g  4732  dfiin3g  4733  resima2  4789  relcnvfld  5008  uniabio  5034  fntpg  5115  dffn5im  5399  dfimafn2  5403  fncnvima2  5473  fmptcof  5519  fcoconst  5523  fnasrng  5532  ffnov  5807  fnovim  5811  fnrnov  5848  foov  5849  funimassov  5852  ovelimab  5853  ofc12  5933  caofinvl  5935  dftpos3  6089  tfr0dm  6149  rdgisucinc  6212  oasuc  6290  ecinxp  6434  phplem1  6675  exmidpw  6731  unfiin  6743  fidcenumlemr  6771  0ct  6907  ctmlemr  6908  indpi  7051  nqnq0pi  7147  nq0m0r  7165  addnqpr1  7271  recexgt0sr  7469  recidpipr  7543  recidpirq  7545  axrnegex  7564  nntopi  7579  cnref1o  9290  fztp  9699  fseq1m1p1  9716  frecuzrdgrrn  10022  frecuzrdgsuc  10028  frecuzrdgsuctlem  10037  seq3val  10072  seqvalcd  10073  fser0const  10130  mulexpzap  10174  expaddzap  10178  bcp1m1  10352  cjexp  10506  rexuz3  10602  bdtri  10850  climconst  10898  sumfct  10982  zsumdc  10992  fsum3  10995  sum0  10996  fsumcnv  11045  mertenslem2  11144  ef0lem  11164  efzval  11187  efival  11237  sinbnd  11257  cosbnd  11258  eucalgval  11528  eucalginv  11530  eucalglt  11531  eucalgcvga  11532  eucalg  11533  sqpweven  11645  2sqpwodd  11646  dfphi2  11688  phimullem  11693  ennnfonelemhdmp1  11714  ennnfonelemkh  11717  ressid2  11800  ressval2  11801  topnvalg  11914  istps  11981  cldval  12050  ntrfval  12051  clsfval  12052  neifval  12091  restbasg  12119  tgrest  12120  txval  12205  upxp  12222  uptx  12224  txrest  12226  lmcn2  12230  cnmpt2t  12243  cnmpt2res  12247  imasnopn  12249  psmetxrge0  12260  xmetge0  12293  isxms  12379  isms  12381  bdxmet  12429  qtopbasss  12443  cnblcld  12457  negfcncf  12501  dvfvalap  12523  eldvap  12524  dvidlemap  12533  nninfsellemqall  12795