Theorem eqtr3 1497

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr3.1	|- A = B
eqtr3.2	|- A = C

Assertion

Ref	Expression
eqtr3	|- B = C

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqtr3.1	. . 3 |- A = B
2	1	eqcomi 1479	. 2 |- B = A
3		eqtr3.2	. 2 |- A = C
4	2, 3	eqtr 1495	1 |- B = C

Syntax hints:   = wceq 956

This theorem is referenced by:  3eqtrr 1500  3eqtr3 1503  3eqtr3r 1504  unundi 2191  unundir 2192  inindi 2227  inindir 2228  dfin4 2248  difun1 2263  dfrab2 2274  dif0 2335  undif1 2340  difdifdir 2346  intmin2 2557  univ 2909  orduniss2 3090  dmsnsnsn 3329  dmres 3380  rnresi 3418  rnresv 3491  resdmres 3497  coi2 3511  isarep2 3578  ssimaex 3768  fvsnun1 3795  tz7.44-2 3929  caopr31 4062  ecqs 4297  ecopoprtrn 4311  limensuci 4506  pssnn 4534  unir1 4667  rankbnd2 4704  zorn2lem4 4791  iundom 4812  alephsuc2 4881  distrpq 5067  halfpq 5082  addclprlem2 5119  mulgt0sr 5214  subid 5391  neg11 5406  negdi 5448  nneo 6197  dfuz 6202  uzrdgval 6302  seq00 6550  binom2 6644  binom2aOLD 6645  discrlem1 6656  nnesq 6662  sqrlem11 6683  sqr1 6716  cjmul 6789  abssub 6846  abs3lem 6901  abslem2i 6908  facnnt 6933  fac0 6934  faclbnd4lem1 6948  climuz0 7108  isumnn0nna 7208  isummulc1a 7214  fnsmnt 7226  0.999... 7246  dsupivthlem 7291  dfef2 7307  efcvg 7314  efaddlem6 7343  eirrlem2 7390  eirrlem3 7391  eflt 7406  efcnlem2 7420  sin0ALT 7445  efivalt 7447  sin01bndlem1 7467  sin01bndlem3 7469  cos2bnd 7475  sin4lt0 7481  acdc2lem2 7489  acdc5lem2 7492  unbenlem 7504  alephsuc3 7585  metres 7823  tgioo 7915  qdensere2 7916  ipval2 8357  ipdirilem 8488  ipasslem10 8499  sincos6thpi 8711  dfrelog 8756  pilog 8768  hisubcom 8970  normlem0 8975  normlem3 8978  normsub 9008  norm3dif 9014  norm3lem 9016  polid2 9024  projlem3 9188  projlem4 9189  pjthlem5 9223  chdmj1 9404  chjjdir 9447  spansn0 9464  pjoml2 9528  pjoml4 9530  cmbr3 9543  qlaxr3 9577  honpcan 9751  honpncan 9753  lnopunilem1 9935  lnophmlem2 9942  adjbdlnb 10017  pjbdln 10076  pjclem1 10123  pjclem3 10125  pjc 10128  cvmd 10251  atoml 10309  atabs2 10329  mddmdin0 10358

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain