Theorem eqtr3id 2224

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr3id.1	|- B = A
eqtr3id.2	|- ( ph -> B = C )

Assertion

Ref	Expression
eqtr3id	|- ( ph -> A = C )

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 |- B = A
2	1	eqcomi 2181	. 2 |- A = B
3		eqtr3id.2	. 2 |- ( ph -> B = C )
4	2, 3	eqtrid 2222	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3g  2233  csbeq1a  3066  ssdifeq0  3505  pofun  4312  opabbi2dv  4776  funimaexg  5300  fresin  5394  f1imacnv  5478  foimacnv  5479  fsn2  5690  fmptpr  5708  funiunfvdm  5763  funiunfvdmf  5764  fcof1o  5789  f1opw2  6076  fnexALT  6111  eqerlem  6565  pmresg  6675  mapsn  6689  fopwdom  6835  mapen  6845  fiintim  6927  xpfi  6928  sbthlemi8  6962  sbthlemi9  6963  ctssdccl  7109  exmidfodomrlemim  7199  mul02  8343  recdivap  8674  fzpreddisj  10070  fzshftral  10107  qbtwnrelemcalc  10255  frec2uzrdg  10408  frecuzrdgrcl  10409  frecuzrdgsuc  10413  frecuzrdgrclt  10414  frecuzrdgg  10415  binom3  10637  bcn2  10743  hashfz1  10762  hashunlem  10783  hashfacen  10815  cnrecnv  10918  resqrexlemnm  11026  amgm2  11126  2zsupmax  11233  xrmaxltsup  11265  xrmaxadd  11268  xrbdtri  11283  fisumss  11399  fsumcnv  11444  telfsumo  11473  fsumiun  11484  arisum2  11506  fprodssdc  11597  fprodsplitdc  11603  fprodsplit  11604  fprodcnv  11632  ege2le3  11678  efgt1p  11703  cos01bnd  11765  suprzubdc  11952  dfgcd3  12010  eucalgval  12053  sqrt2irrlem  12160  pcid  12322  setsslid  12512  ressinbasd  12532  xpsff1o  12767  grpressid  12930  baspartn  13520  txdis1cn  13748  cnmpt21  13761  cnmpt22  13764  hmeores  13785  metreslem  13850  remetdval  14009  dvfvalap  14120  binom4  14367  1lgs  14414  lgs1  14415  lgseisenlem1  14420  lgseisenlem2  14421  nninfsellemqall  14734