Theorem eqtr3id 2285

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

Hypotheses

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

Assertion

Ref	Expression
eqtr3id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2242	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2283	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  3eqtr3g  2294  csbeq1a  3156  ssdifeq0  3607  pofun  4452  opabbi2dv  4924  funimaexg  5460  fresin  5563  f1imacnv  5651  foimacnv  5652  fsn2  5873  fmptpr  5898  funiunfvdm  5959  funiunfvdmf  5960  fcof1o  5985  f1opw2  6286  fnexALT  6330  eqerlem  6828  pmresg  6947  mapsn  6962  en2  7102  fopwdom  7126  mapen  7136  fiintim  7228  xpfi  7229  sbthlemi8  7271  sbthlemi9  7272  ctssdccl  7441  exmidfodomrlemim  7543  mul02  8704  recdivap  9038  fzpreddisj  10456  fzshftral  10493  suprzubdc  10649  qbtwnrelemcalc  10668  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  seqf1oglem2  10935  binom3  11072  bcn2  11180  hashfz1  11200  hashunlem  11222  hashfacen  11262  hashtpg  11277  cnrecnv  11654  resqrexlemnm  11762  amgm2  11862  2zsupmax  11970  xrmaxltsup  12002  xrmaxadd  12005  xrbdtri  12020  fisumss  12137  fsumcnv  12182  telfsumo  12211  fsumiun  12222  arisum2  12244  fprodssdc  12335  fprodsplitdc  12341  fprodsplit  12342  fprodcnv  12370  ege2le3  12416  efgt1p  12441  cos01bnd  12503  dfgcd3  12765  eucalgval  12810  sqrt2irrlem  12917  pcid  13081  4sqlem15  13162  4sqlem16  13163  ballotfilemic  13228  setsslid  13381  ressinbasd  13405  xpsff1o  13647  grpressid  13843  gsumf1ofi  14137  gsumconstcmn  14143  crng2idl  14840  znleval  14960  baspartn  15074  txdis1cn  15302  cnmpt21  15315  cnmpt22  15318  hmeores  15339  metreslem  15404  remetdval  15571  dvfvalap  15705  binom4  16004  mpodvdsmulf1o  16018  perfectlem2  16028  1lgs  16076  lgs1  16077  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgsquadlem2  16111  lgsquad2lem2  16115  vtxdfifiun  16452  vtxdumgrfival  16453  nninfsellemqall  16963  nninfnfiinf  16971  repiecege0  16981