Theorem eqtr3id 2276

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3g  2285  csbeq1a  3134  ssdifeq0  3575  pofun  4407  opabbi2dv  4877  funimaexg  5411  fresin  5512  f1imacnv  5597  foimacnv  5598  fsn2  5817  fmptpr  5841  funiunfvdm  5899  funiunfvdmf  5900  fcof1o  5925  f1opw2  6224  fnexALT  6268  eqerlem  6728  pmresg  6840  mapsn  6854  en2  6993  fopwdom  7017  mapen  7027  fiintim  7116  xpfi  7117  sbthlemi8  7154  sbthlemi9  7155  ctssdccl  7301  exmidfodomrlemim  7402  mul02  8556  recdivap  8888  fzpreddisj  10296  fzshftral  10333  suprzubdc  10486  qbtwnrelemcalc  10505  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  seqf1oglem2  10772  binom3  10909  bcn2  11016  hashfz1  11035  hashunlem  11057  hashfacen  11090  cnrecnv  11461  resqrexlemnm  11569  amgm2  11669  2zsupmax  11777  xrmaxltsup  11809  xrmaxadd  11812  xrbdtri  11827  fisumss  11943  fsumcnv  11988  telfsumo  12017  fsumiun  12028  arisum2  12050  fprodssdc  12141  fprodsplitdc  12147  fprodsplit  12148  fprodcnv  12176  ege2le3  12222  efgt1p  12247  cos01bnd  12309  dfgcd3  12571  eucalgval  12616  sqrt2irrlem  12723  pcid  12887  4sqlem15  12968  4sqlem16  12969  setsslid  13123  ressinbasd  13147  xpsff1o  13422  grpressid  13634  crng2idl  14535  znleval  14657  baspartn  14764  txdis1cn  14992  cnmpt21  15005  cnmpt22  15008  hmeores  15029  metreslem  15094  remetdval  15261  dvfvalap  15395  binom4  15693  mpodvdsmulf1o  15704  perfectlem2  15714  1lgs  15762  lgs1  15763  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgsquadlem2  15797  lgsquad2lem2  15801  vtxdfifiun  16103  vtxdumgrfival  16104  nninfsellemqall  16553  nninfnfiinf  16561