Theorem eqtr3id 2234

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

Syntax hints:   → wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  3eqtr3g  2243  csbeq1a  3078  ssdifeq0  3517  pofun  4324  opabbi2dv  4788  funimaexg  5312  fresin  5406  f1imacnv  5490  foimacnv  5491  fsn2  5703  fmptpr  5721  funiunfvdm  5777  funiunfvdmf  5778  fcof1o  5803  f1opw2  6090  fnexALT  6125  eqerlem  6579  pmresg  6689  mapsn  6703  fopwdom  6849  mapen  6859  fiintim  6941  xpfi  6942  sbthlemi8  6976  sbthlemi9  6977  ctssdccl  7123  exmidfodomrlemim  7213  mul02  8357  recdivap  8688  fzpreddisj  10084  fzshftral  10121  qbtwnrelemcalc  10269  frec2uzrdg  10422  frecuzrdgrcl  10423  frecuzrdgsuc  10427  frecuzrdgrclt  10428  frecuzrdgg  10429  binom3  10651  bcn2  10757  hashfz1  10776  hashunlem  10797  hashfacen  10829  cnrecnv  10932  resqrexlemnm  11040  amgm2  11140  2zsupmax  11247  xrmaxltsup  11279  xrmaxadd  11282  xrbdtri  11297  fisumss  11413  fsumcnv  11458  telfsumo  11487  fsumiun  11498  arisum2  11520  fprodssdc  11611  fprodsplitdc  11617  fprodsplit  11618  fprodcnv  11646  ege2le3  11692  efgt1p  11717  cos01bnd  11779  suprzubdc  11966  dfgcd3  12024  eucalgval  12067  sqrt2irrlem  12174  pcid  12336  setsslid  12526  ressinbasd  12547  xpsff1o  12786  grpressid  12957  baspartn  13821  txdis1cn  14049  cnmpt21  14062  cnmpt22  14065  hmeores  14086  metreslem  14151  remetdval  14310  dvfvalap  14421  binom4  14668  1lgs  14715  lgs1  14716  lgseisenlem1  14721  lgseisenlem2  14722  nninfsellemqall  15036