Theorem eqtr3id 2243

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 2200	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2241	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3g  2252  csbeq1a  3093  ssdifeq0  3533  pofun  4347  opabbi2dv  4815  funimaexg  5342  fresin  5436  f1imacnv  5521  foimacnv  5522  fsn2  5736  fmptpr  5754  funiunfvdm  5810  funiunfvdmf  5811  fcof1o  5836  f1opw2  6129  fnexALT  6168  eqerlem  6623  pmresg  6735  mapsn  6749  fopwdom  6897  mapen  6907  fiintim  6992  xpfi  6993  sbthlemi8  7030  sbthlemi9  7031  ctssdccl  7177  exmidfodomrlemim  7268  mul02  8413  recdivap  8745  fzpreddisj  10146  fzshftral  10183  suprzubdc  10326  qbtwnrelemcalc  10345  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  seqf1oglem2  10612  binom3  10749  bcn2  10856  hashfz1  10875  hashunlem  10896  hashfacen  10928  cnrecnv  11075  resqrexlemnm  11183  amgm2  11283  2zsupmax  11391  xrmaxltsup  11423  xrmaxadd  11426  xrbdtri  11441  fisumss  11557  fsumcnv  11602  telfsumo  11631  fsumiun  11642  arisum2  11664  fprodssdc  11755  fprodsplitdc  11761  fprodsplit  11762  fprodcnv  11790  ege2le3  11836  efgt1p  11861  cos01bnd  11923  dfgcd3  12177  eucalgval  12222  sqrt2irrlem  12329  pcid  12493  4sqlem15  12574  4sqlem16  12575  setsslid  12729  ressinbasd  12752  xpsff1o  12992  grpressid  13193  crng2idl  14087  znleval  14209  baspartn  14286  txdis1cn  14514  cnmpt21  14527  cnmpt22  14530  hmeores  14551  metreslem  14616  remetdval  14783  dvfvalap  14917  binom4  15215  mpodvdsmulf1o  15226  perfectlem2  15236  1lgs  15284  lgs1  15285  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem2  15319  lgsquad2lem2  15323  nninfsellemqall  15659