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  hashtpg  11112  cnrecnv  11475  resqrexlemnm  11583  amgm2  11683  2zsupmax  11791  xrmaxltsup  11823  xrmaxadd  11826  xrbdtri  11841  fisumss  11958  fsumcnv  12003  telfsumo  12032  fsumiun  12043  arisum2  12065  fprodssdc  12156  fprodsplitdc  12162  fprodsplit  12163  fprodcnv  12191  ege2le3  12237  efgt1p  12262  cos01bnd  12324  dfgcd3  12586  eucalgval  12631  sqrt2irrlem  12738  pcid  12902  4sqlem15  12983  4sqlem16  12984  setsslid  13138  ressinbasd  13162  xpsff1o  13437  grpressid  13649  crng2idl  14551  znleval  14673  baspartn  14780  txdis1cn  15008  cnmpt21  15021  cnmpt22  15024  hmeores  15045  metreslem  15110  remetdval  15277  dvfvalap  15411  binom4  15709  mpodvdsmulf1o  15720  perfectlem2  15730  1lgs  15778  lgs1  15779  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgsquadlem2  15813  lgsquad2lem2  15817  vtxdfifiun  16154  vtxdumgrfival  16155  nninfsellemqall  16643  nninfnfiinf  16651