Theorem cleq2 1110

Description: Equality implies equivalence of equalities.

Assertion

Ref	Expression
cleq2	⊢ (A = B → (C = A ↔ C = B))

Proof of Theorem cleq2

Step	Hyp	Ref	Expression
1		cleq1 1107	. 2 ⊢ (A = B → (A = C ↔ B = C))
2		cleqcom 1103	. 2 ⊢ (C = A ↔ A = C)
3		cleqcom 1103	. 2 ⊢ (C = B ↔ B = C)
4	1, 2, 3	3bitr4g 428	1 ⊢ (A = B → (C = A ↔ C = B))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091

This theorem is referenced by:  cleq2i 1111  cleq2d 1112  cleq12 1113  eleq1 1149  neeq2 1195  eqvinc 1407  alexeq 1409  ceqex 1410  eueq 1427  moeq3 1432  mo2icl 1434  sneq 1816  preqr1 1872  prel12 1875  dtru 1889  opthg 1899  euuni 1954  reuuni2 1956  ideqg 2126  solin 2145  so 2152  dfwe2 2187  ordequn 2331  findsg 2398  tfindsg 2402  resieq 2581  funsn 2690  fneq2 2719  foeq3 2786  f1oco 2816  tz6.12f 2844  tz6.12i 2847  funbrfv 2852  funopfvg 2854  fnfvbr 2855  fvelima 2859  fvopab2 2878  fvelrn 2883  f1fvf 2917  f1fveq 2918  isowe 2941  f1oweOLD 2944  rdgeq2 2973  caoprcan 3069  oawordeu 3157  eceqopreq 3249  2dom 3332  fundmen 3333  nneneq 3408  aceq5 3563  kmlem4 3583  kmlem14 3593  cardcf 3706  ltsopq 3869  ltexpq 3874  halfpq 3876  ltsosr 3997  map2psrpr 4014  ltsor 4055  axrecex 4079  addcant 4122  negeu 4124  subval 4134  subadd 4143  subaddt 4145  negcon1t 4167  subeq0t 4169  mulcant 4208  receu 4215  divval 4217  divmul 4218  divmult 4220  rec11 4262  redivcl 4274  nnleltp1t 4448  crut 4531  nn0ind 4612  sqe11t 4705  nn0opth2t 4726  replimt 4798  climuni 4884  hvsubeq0t 5040  hvsubaddt 5042  normsub0t 5085  hlimuni 5144  occllem5 5184  omls 5251  5oalem4 5547  pjclem4a 5652  pj3lem1 5658  strlem4 5695  jplem1 5701

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