Theorem eqtr3id 2240

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 2197	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2238	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3g  2249  csbeq1a  3089  ssdifeq0  3529  pofun  4343  opabbi2dv  4811  funimaexg  5338  fresin  5432  f1imacnv  5517  foimacnv  5518  fsn2  5732  fmptpr  5750  funiunfvdm  5806  funiunfvdmf  5807  fcof1o  5832  f1opw2  6124  fnexALT  6163  eqerlem  6618  pmresg  6730  mapsn  6744  fopwdom  6892  mapen  6902  fiintim  6985  xpfi  6986  sbthlemi8  7023  sbthlemi9  7024  ctssdccl  7170  exmidfodomrlemim  7261  mul02  8406  recdivap  8737  fzpreddisj  10137  fzshftral  10174  qbtwnrelemcalc  10324  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  seqf1oglem2  10591  binom3  10728  bcn2  10835  hashfz1  10854  hashunlem  10875  hashfacen  10907  cnrecnv  11054  resqrexlemnm  11162  amgm2  11262  2zsupmax  11369  xrmaxltsup  11401  xrmaxadd  11404  xrbdtri  11419  fisumss  11535  fsumcnv  11580  telfsumo  11609  fsumiun  11620  arisum2  11642  fprodssdc  11733  fprodsplitdc  11739  fprodsplit  11740  fprodcnv  11768  ege2le3  11814  efgt1p  11839  cos01bnd  11901  suprzubdc  12089  dfgcd3  12147  eucalgval  12192  sqrt2irrlem  12299  pcid  12462  4sqlem15  12543  4sqlem16  12544  setsslid  12669  ressinbasd  12692  xpsff1o  12932  grpressid  13133  crng2idl  14027  znleval  14141  baspartn  14218  txdis1cn  14446  cnmpt21  14459  cnmpt22  14462  hmeores  14483  metreslem  14548  remetdval  14707  dvfvalap  14835  binom4  15111  1lgs  15159  lgs1  15160  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  nninfsellemqall  15505