Theorem eqtr3id 2278

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3g  2287  csbeq1a  3136  ssdifeq0  3577  pofun  4409  opabbi2dv  4879  funimaexg  5414  fresin  5515  f1imacnv  5600  foimacnv  5601  fsn2  5821  fmptpr  5846  funiunfvdm  5904  funiunfvdmf  5905  fcof1o  5930  f1opw2  6229  fnexALT  6273  eqerlem  6733  pmresg  6845  mapsn  6859  en2  6998  fopwdom  7022  mapen  7032  fiintim  7123  xpfi  7124  sbthlemi8  7163  sbthlemi9  7164  ctssdccl  7310  exmidfodomrlemim  7412  mul02  8566  recdivap  8898  fzpreddisj  10306  fzshftral  10343  suprzubdc  10497  qbtwnrelemcalc  10516  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  seqf1oglem2  10783  binom3  10920  bcn2  11027  hashfz1  11046  hashunlem  11068  hashfacen  11101  cnrecnv  11472  resqrexlemnm  11580  amgm2  11680  2zsupmax  11788  xrmaxltsup  11820  xrmaxadd  11823  xrbdtri  11838  fisumss  11955  fsumcnv  12000  telfsumo  12029  fsumiun  12040  arisum2  12062  fprodssdc  12153  fprodsplitdc  12159  fprodsplit  12160  fprodcnv  12188  ege2le3  12234  efgt1p  12259  cos01bnd  12321  dfgcd3  12583  eucalgval  12628  sqrt2irrlem  12735  pcid  12899  4sqlem15  12980  4sqlem16  12981  setsslid  13135  ressinbasd  13159  xpsff1o  13434  grpressid  13646  crng2idl  14548  znleval  14670  baspartn  14777  txdis1cn  15005  cnmpt21  15018  cnmpt22  15021  hmeores  15042  metreslem  15107  remetdval  15274  dvfvalap  15408  binom4  15706  mpodvdsmulf1o  15717  perfectlem2  15727  1lgs  15775  lgs1  15776  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgsquadlem2  15810  lgsquad2lem2  15814  vtxdfifiun  16151  vtxdumgrfival  16152  nninfsellemqall  16634  nninfnfiinf  16642