Theorem eqtr3id 2217

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  3eqtr3g  2226  csbeq1a  3058  ssdifeq0  3497  pofun  4297  opabbi2dv  4760  funimaexg  5282  fresin  5376  f1imacnv  5459  foimacnv  5460  fsn2  5670  fmptpr  5688  funiunfvdm  5742  funiunfvdmf  5743  fcof1o  5768  f1opw2  6055  fnexALT  6090  eqerlem  6544  pmresg  6654  mapsn  6668  fopwdom  6814  mapen  6824  fiintim  6906  xpfi  6907  sbthlemi8  6941  sbthlemi9  6942  ctssdccl  7088  exmidfodomrlemim  7178  mul02  8306  recdivap  8635  fzpreddisj  10027  fzshftral  10064  qbtwnrelemcalc  10212  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  binom3  10593  bcn2  10698  hashfz1  10717  hashunlem  10739  hashfacen  10771  cnrecnv  10874  resqrexlemnm  10982  amgm2  11082  2zsupmax  11189  xrmaxltsup  11221  xrmaxadd  11224  xrbdtri  11239  fisumss  11355  fsumcnv  11400  telfsumo  11429  fsumiun  11440  arisum2  11462  fprodssdc  11553  fprodsplitdc  11559  fprodsplit  11560  fprodcnv  11588  ege2le3  11634  efgt1p  11659  cos01bnd  11721  suprzubdc  11907  dfgcd3  11965  eucalgval  12008  sqrt2irrlem  12115  pcid  12277  setsslid  12466  baspartn  12842  txdis1cn  13072  cnmpt21  13085  cnmpt22  13088  hmeores  13109  metreslem  13174  remetdval  13333  dvfvalap  13444  binom4  13691  1lgs  13738  lgs1  13739  nninfsellemqall  14048