Theorem eqtr3id 2276

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3g  2285  csbeq1a  3133  ssdifeq0  3574  pofun  4402  opabbi2dv  4870  funimaexg  5404  fresin  5503  f1imacnv  5588  foimacnv  5589  fsn2  5808  fmptpr  5830  funiunfvdm  5886  funiunfvdmf  5887  fcof1o  5912  f1opw2  6210  fnexALT  6254  eqerlem  6709  pmresg  6821  mapsn  6835  en2  6971  fopwdom  6993  mapen  7003  fiintim  7089  xpfi  7090  sbthlemi8  7127  sbthlemi9  7128  ctssdccl  7274  exmidfodomrlemim  7375  mul02  8529  recdivap  8861  fzpreddisj  10263  fzshftral  10300  suprzubdc  10451  qbtwnrelemcalc  10470  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  seqf1oglem2  10737  binom3  10874  bcn2  10981  hashfz1  11000  hashunlem  11021  hashfacen  11053  cnrecnv  11416  resqrexlemnm  11524  amgm2  11624  2zsupmax  11732  xrmaxltsup  11764  xrmaxadd  11767  xrbdtri  11782  fisumss  11898  fsumcnv  11943  telfsumo  11972  fsumiun  11983  arisum2  12005  fprodssdc  12096  fprodsplitdc  12102  fprodsplit  12103  fprodcnv  12131  ege2le3  12177  efgt1p  12202  cos01bnd  12264  dfgcd3  12526  eucalgval  12571  sqrt2irrlem  12678  pcid  12842  4sqlem15  12923  4sqlem16  12924  setsslid  13078  ressinbasd  13102  xpsff1o  13377  grpressid  13589  crng2idl  14489  znleval  14611  baspartn  14718  txdis1cn  14946  cnmpt21  14959  cnmpt22  14962  hmeores  14983  metreslem  15048  remetdval  15215  dvfvalap  15349  binom4  15647  mpodvdsmulf1o  15658  perfectlem2  15668  1lgs  15716  lgs1  15717  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgsquadlem2  15751  lgsquad2lem2  15755  nninfsellemqall  16340  nninfnfiinf  16348