Theorem eqtr3 1121

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	cleqcomi 1105	. 2 |- B = A
3		eqtr3.2	. 2 |- A = C
4	2, 3	eqtr 1119	1 |- B = C

Syntax hints:   = wceq 1091

This theorem is referenced by:  3eqtr3 1124  3eqtr3r 1125  unundi 1619  unundir 1620  inindi 1654  inindir 1655  dfin4 1673  indif 1675  difun1 1687  dfrab2 1696  dif0 1756  undif1 1761  difdifdir 1765  univ 1964  dmsnsnsn 2548  dmres 2584  rnresi 2614  coi2 2666  funimacnv 2711  tz7.44-2 2967  caopr31 3076  1st2val 3097  ecqs 3233  ecopoprtrn 3247  limensuci 3401  pssnn 3428  unir1 3511  zornlem4 3606  fodomb 3615  cardval2 3661  alephsuc2 3686  distrpq 3861  halfpq 3876  addclprlem2 3913  mulgt0sr 4008  subdi 4182  negdi 4193  uzrdgval 4657  binom 4712  discrlem1 4713  nneo 4719  nnesq 4720  sqrlem11 4741  sqr1 4771  cjmul 4819  cjmulval 4822  abssub 4845  sqabsadd 4847  abs3lem 4861  abslem2i 4866  ruclem1 4885  ruclem3 4887  ruclem7 4891  alephsuc3 4955  normlem0 5062  normlem3 5065  normsub 5089  norm3dif 5094  norm3lem 5096  projlem3 5195  projlem4 5196  chdmj1 5402  pjoml2 5495  pjoml4 5497  cmbr3 5509  fh1 5518  fh2 5519  qlaxr3 5529  pjinorm 5567  hosd1 5623

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org