Theorem eqtr3id 2285

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3g  2294  csbeq1a  3156  ssdifeq0  3610  pofun  4459  opabbi2dv  4931  funimaexg  5468  fresin  5571  f1imacnv  5659  foimacnv  5660  fsn2  5885  fmptpr  5910  funiunfvdm  5972  funiunfvdmf  5973  fcof1o  5998  f1opw2  6299  fnexALT  6344  eqerlem  6842  pmresg  6961  mapsn  6976  en2  7116  fopwdom  7140  mapen  7150  fiintim  7242  xpfi  7243  sbthlemi8  7286  sbthlemi9  7287  ctssdccl  7457  exmidfodomrlemim  7559  mul02  8721  recdivap  9056  fzpreddisj  10495  fzshftral  10532  suprzubdc  10688  qbtwnrelemcalc  10707  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgg  10874  seqf1oglem2  10978  binom3  11115  bcn2  11224  hashfz1  11244  hashunlem  11266  hashfacen  11306  hashtpg  11321  cnrecnv  11698  resqrexlemnm  11806  amgm2  11907  2zsupmax  12015  xrmaxltsup  12049  xrmaxadd  12052  xrbdtri  12067  fisumss  12184  fsumcnv  12229  telfsumo  12258  fsumiun  12269  arisum2  12291  fprodssdc  12382  fprodsplitdc  12388  fprodsplit  12389  fprodcnv  12417  ege2le3  12463  efgt1p  12488  cos01bnd  12550  dfgcd3  12812  eucalgval  12857  sqrt2irrlem  12965  pcid  13132  4sqlem15  13213  4sqlem16  13214  ballotfilemic  13308  setsslid  13461  ressinbasd  13487  xpsff1o  13729  grpressid  13925  gsumf1ofi  14250  gsumconstcmn  14266  crng2idl  14977  znleval  15097  psrass1filem  15177  baspartn  15276  txdis1cn  15504  cnmpt21  15517  cnmpt22  15520  hmeores  15541  metreslem  15606  remetdval  15773  dvfvalap  15907  binom4  16219  mpodvdsmulf1o  16284  ppiqub  16293  chtublem  16295  perfectlem2  16300  bposlem6  16316  bposlem9  16319  1lgs  16367  lgs1  16368  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgsquadlem2  16402  lgsquad2lem2  16406  vtxdfifiun  16743  vtxdumgrfival  16744  nninfsellemqall  17264  nninfnfiinf  17272  repiecege0  17282