Theorem eqtr3id 2253

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  3eqtr3g  2262  csbeq1a  3106  ssdifeq0  3547  pofun  4367  opabbi2dv  4835  funimaexg  5367  fresin  5466  f1imacnv  5551  foimacnv  5552  fsn2  5767  fmptpr  5789  funiunfvdm  5845  funiunfvdmf  5846  fcof1o  5871  f1opw2  6165  fnexALT  6209  eqerlem  6664  pmresg  6776  mapsn  6790  en2  6926  fopwdom  6948  mapen  6958  fiintim  7043  xpfi  7044  sbthlemi8  7081  sbthlemi9  7082  ctssdccl  7228  exmidfodomrlemim  7325  mul02  8479  recdivap  8811  fzpreddisj  10213  fzshftral  10250  suprzubdc  10401  qbtwnrelemcalc  10420  frec2uzrdg  10576  frecuzrdgrcl  10577  frecuzrdgsuc  10581  frecuzrdgrclt  10582  frecuzrdgg  10583  seqf1oglem2  10687  binom3  10824  bcn2  10931  hashfz1  10950  hashunlem  10971  hashfacen  11003  cnrecnv  11296  resqrexlemnm  11404  amgm2  11504  2zsupmax  11612  xrmaxltsup  11644  xrmaxadd  11647  xrbdtri  11662  fisumss  11778  fsumcnv  11823  telfsumo  11852  fsumiun  11863  arisum2  11885  fprodssdc  11976  fprodsplitdc  11982  fprodsplit  11983  fprodcnv  12011  ege2le3  12057  efgt1p  12082  cos01bnd  12144  dfgcd3  12406  eucalgval  12451  sqrt2irrlem  12558  pcid  12722  4sqlem15  12803  4sqlem16  12804  setsslid  12958  ressinbasd  12981  xpsff1o  13256  grpressid  13468  crng2idl  14368  znleval  14490  baspartn  14597  txdis1cn  14825  cnmpt21  14838  cnmpt22  14841  hmeores  14862  metreslem  14927  remetdval  15094  dvfvalap  15228  binom4  15526  mpodvdsmulf1o  15537  perfectlem2  15547  1lgs  15595  lgs1  15596  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgsquadlem2  15630  lgsquad2lem2  15634  nninfsellemqall  16093  nninfnfiinf  16101