Theorem eqtr4 1122

Description: An equality transitivity inference.

Hypotheses

Ref	Expression
eqtr4.1	⊢ A = B
eqtr4.2	⊢ C = B

Assertion

Ref	Expression
eqtr4	⊢ A = C

Proof of Theorem eqtr4

Step	Hyp	Ref	Expression
1		eqtr4.1	. 2 ⊢ A = B
2		eqtr4.2	. . 3 ⊢ C = B
3	2	cleqcomi 1105	. 2 ⊢ B = C
4	1, 3	eqtr 1119	1 ⊢ A = C

Syntax hints:   = wceq 1091

This theorem is referenced by:  3eqtr4 1126  3eqtr4r 1127  elabs2 1457  dfdif2 1495  difeqri 1589  difrab 1695  pw0 1882  dfint2 1967  intmin2 1984  uniiun 2026  intiin 2027  xpundi 2461  xpundir 2462  resopab 2598  cnvcnv 2661  funimacnv 2711  abrexex2 2915  dmoprab 3031  fnoprval 3042  oprabval4g 3053  1st2val 3097  df1st2 3098  df2o2 3112  o1p1e2 3143  map0e 3266  inf5 3472  unir1 3511  rankpr 3536  kmlem10 3589  cardval2 3661  cf0 3705  ltexpq 3874  halfpq 3876  genpdm 3899  prlem936a 3947  m1p1sr 3995  m1m1sr 3996  mappsrpr 4012  dfcnqs 4056  axrecex 4079  sub4 4206  ltreci 4409  lt2sq 4414  2p2e4 4488  3p2e5 4492  3p3e6 4493  4p2e6 4494  4p3e7 4495  4p4e8 4496  5p2e7 4497  5p3e8 4498  5p4e9 4499  6p2e8 4500  6p3e9 4501  7p2e9 4502  irec 4526  crmult 4530  nnz 4582  nn0z 4583  seqsuclem 4669  discrlem1 4713  sqrval 4729  sqrlem11 4741  cjmul 4819  cjmulval 4822  cjneg 4827  abscj 4844  absre 4854  abstri 4859  abs3dif 4860  ruclem13 4897  ruclem17 4901  infxpidmlem9 4941  alephsuc3 4955  hvsubass 5027  normlem0 5062  normlem1 5063  normlem2 5064  normlem4 5066  normlem8 5071  bcseq 5073  norm-ii 5086  norm3dif 5094  normpar2 5100  ocvalt 5161  occllem1 5180  projlem3 5195  projlem4 5196  pjthlem1 5225  pjthlem5 5229  pjthlem6 5230  pjthlem14 5238  spanvalt 5300  hsupval2t 5301  sshjvalt 5321  sshjval3t 5327  shsumval3 5362  hosmvalt 5487  hodmvalt 5488  cmcm2 5502  fh2 5519  qlaxr3 5529  pjinorm 5567  pjcj 5575  ho0 5612  hosd2 5624  pjclem3 5651

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