Theorem eqtr3id 2224

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3g  2233  csbeq1a  3068  ssdifeq0  3507  pofun  4314  opabbi2dv  4778  funimaexg  5302  fresin  5396  f1imacnv  5480  foimacnv  5481  fsn2  5692  fmptpr  5710  funiunfvdm  5766  funiunfvdmf  5767  fcof1o  5792  f1opw2  6079  fnexALT  6114  eqerlem  6568  pmresg  6678  mapsn  6692  fopwdom  6838  mapen  6848  fiintim  6930  xpfi  6931  sbthlemi8  6965  sbthlemi9  6966  ctssdccl  7112  exmidfodomrlemim  7202  mul02  8346  recdivap  8677  fzpreddisj  10073  fzshftral  10110  qbtwnrelemcalc  10258  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  binom3  10640  bcn2  10746  hashfz1  10765  hashunlem  10786  hashfacen  10818  cnrecnv  10921  resqrexlemnm  11029  amgm2  11129  2zsupmax  11236  xrmaxltsup  11268  xrmaxadd  11271  xrbdtri  11286  fisumss  11402  fsumcnv  11447  telfsumo  11476  fsumiun  11487  arisum2  11509  fprodssdc  11600  fprodsplitdc  11606  fprodsplit  11607  fprodcnv  11635  ege2le3  11681  efgt1p  11706  cos01bnd  11768  suprzubdc  11955  dfgcd3  12013  eucalgval  12056  sqrt2irrlem  12163  pcid  12325  setsslid  12515  ressinbasd  12535  xpsff1o  12773  grpressid  12936  baspartn  13589  txdis1cn  13817  cnmpt21  13830  cnmpt22  13833  hmeores  13854  metreslem  13919  remetdval  14078  dvfvalap  14189  binom4  14436  1lgs  14483  lgs1  14484  lgseisenlem1  14489  lgseisenlem2  14490  nninfsellemqall  14803