New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqeq1d | GIF version |
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.) |
Ref | Expression |
---|---|
eqeq1d.1 | ⊢ (φ → A = B) |
Ref | Expression |
---|---|
eqeq1d | ⊢ (φ → (A = C ↔ B = C)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1d.1 | . 2 ⊢ (φ → A = B) | |
2 | eqeq1 2359 | . 2 ⊢ (A = B → (A = C ↔ B = C)) | |
3 | 1, 2 | syl 15 | 1 ⊢ (φ → (A = C ↔ B = C)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 = wceq 1642 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: sbceq2g 3158 csbhypf 3171 csbiebt 3172 csbiebg 3175 disjssun 3608 sneqrg 3874 preqr2g 4126 preq12b 4127 preq12bg 4128 opkthg 4131 iotaeq 4347 iotabi 4348 eladdci 4399 addcid1 4405 elsuc 4413 addcass 4415 nndisjeq 4429 preaddccan2lem1 4454 tfinltfinlem1 4500 sucoddeven 4511 sfin01 4528 phiall 4618 xpcan 5057 xpcan2 5058 dmsnopg 5066 fneq1 5173 fnun 5189 fnresdisj 5193 fnimadisj 5203 foeq1 5265 foco 5279 fvun1 5379 fvco2 5382 fnasrn 5417 dffo3 5422 fvsng 5446 fconstfv 5456 dff13f 5472 f1fveq 5473 f1elima 5474 ov3 5599 ovelimab 5610 caovcan 5628 caovmo 5645 brcupg 5814 brcomposeg 5819 brdisjg 5821 qsdisj 5995 mapsn 6026 endisj 6051 enadj 6060 enmap2lem3 6065 enmap1lem3 6071 enprmaplem5 6080 enprmaplem6 6081 1cnc 6139 ncdisjeq 6148 addceq0 6219 letc 6230 ce0lenc1 6238 muc0or 6251 csucex 6258 addccan2nclem2 6263 nncdiv3 6275 nnc3n3p1 6276 nchoicelem1 6287 nchoicelem9 6295 nchoicelem14 6300 nchoicelem16 6302 nchoicelem17 6303 nchoice 6306 |
Copyright terms: Public domain | W3C validator |