Theorem eqtr3id 2212

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  3eqtr3g  2221  csbeq1a  3053  ssdifeq0  3490  pofun  4289  opabbi2dv  4752  funimaexg  5271  fresin  5365  f1imacnv  5448  foimacnv  5449  fsn2  5658  fmptpr  5676  funiunfvdm  5730  funiunfvdmf  5731  fcof1o  5756  f1opw2  6043  fnexALT  6078  eqerlem  6528  pmresg  6638  mapsn  6652  fopwdom  6798  mapen  6808  fiintim  6890  xpfi  6891  sbthlemi8  6925  sbthlemi9  6926  ctssdccl  7072  exmidfodomrlemim  7153  mul02  8281  recdivap  8610  fzpreddisj  10002  fzshftral  10039  qbtwnrelemcalc  10187  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  binom3  10568  bcn2  10673  hashfz1  10692  hashunlem  10713  hashfacen  10745  cnrecnv  10848  resqrexlemnm  10956  amgm2  11056  2zsupmax  11163  xrmaxltsup  11195  xrmaxadd  11198  xrbdtri  11213  fisumss  11329  fsumcnv  11374  telfsumo  11403  fsumiun  11414  arisum2  11436  fprodssdc  11527  fprodsplitdc  11533  fprodsplit  11534  fprodcnv  11562  ege2le3  11608  efgt1p  11633  cos01bnd  11695  suprzubdc  11881  dfgcd3  11939  eucalgval  11982  sqrt2irrlem  12089  pcid  12251  setsslid  12440  baspartn  12648  txdis1cn  12878  cnmpt21  12891  cnmpt22  12894  hmeores  12915  metreslem  12980  remetdval  13139  dvfvalap  13250  binom4  13497  1lgs  13544  lgs1  13545  nninfsellemqall  13855