Theorem eqtr3id 2243

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 2200	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2241	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3g  2252  csbeq1a  3093  ssdifeq0  3534  pofun  4348  opabbi2dv  4816  funimaexg  5343  fresin  5439  f1imacnv  5524  foimacnv  5525  fsn2  5739  fmptpr  5757  funiunfvdm  5813  funiunfvdmf  5814  fcof1o  5839  f1opw2  6133  fnexALT  6177  eqerlem  6632  pmresg  6744  mapsn  6758  fopwdom  6906  mapen  6916  fiintim  7001  xpfi  7002  sbthlemi8  7039  sbthlemi9  7040  ctssdccl  7186  exmidfodomrlemim  7282  mul02  8432  recdivap  8764  fzpreddisj  10165  fzshftral  10202  suprzubdc  10345  qbtwnrelemcalc  10364  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgg  10527  seqf1oglem2  10631  binom3  10768  bcn2  10875  hashfz1  10894  hashunlem  10915  hashfacen  10947  cnrecnv  11094  resqrexlemnm  11202  amgm2  11302  2zsupmax  11410  xrmaxltsup  11442  xrmaxadd  11445  xrbdtri  11460  fisumss  11576  fsumcnv  11621  telfsumo  11650  fsumiun  11661  arisum2  11683  fprodssdc  11774  fprodsplitdc  11780  fprodsplit  11781  fprodcnv  11809  ege2le3  11855  efgt1p  11880  cos01bnd  11942  dfgcd3  12204  eucalgval  12249  sqrt2irrlem  12356  pcid  12520  4sqlem15  12601  4sqlem16  12602  setsslid  12756  ressinbasd  12779  xpsff1o  13053  grpressid  13265  crng2idl  14165  znleval  14287  baspartn  14394  txdis1cn  14622  cnmpt21  14635  cnmpt22  14638  hmeores  14659  metreslem  14724  remetdval  14891  dvfvalap  15025  binom4  15323  mpodvdsmulf1o  15334  perfectlem2  15344  1lgs  15392  lgs1  15393  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgsquadlem2  15427  lgsquad2lem2  15431  nninfsellemqall  15770  nninfnfiinf  15778