New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqeq2 | Unicode version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2359 | . 2 | |
2 | eqcom 2355 | . 2 | |
3 | eqcom 2355 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 279 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wceq 1642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 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: eqeq2i 2363 eqeq2d 2364 eqeq12 2365 eleq1 2413 neeq2 2525 alexeq 2968 ceqex 2969 pm13.183 2979 eqeu 3007 moeq3 3013 mo2icl 3015 mob2 3016 euind 3023 reu6i 3027 reuind 3039 sbc2or 3054 sbc5 3070 csbiebg 3175 eqif 3695 sneq 3744 preqr1 4124 preqr2g 4126 preq12bg 4128 opkelidkg 4274 iota5 4359 nndisjeq 4429 lefinlteq 4463 ltfintri 4466 evenodddisjlem1 4515 ideqg 4868 ideqg2 4869 fneq2 5174 foeq3 5267 fvelimab 5370 fvopab4t 5385 dff13f 5472 f1fveq 5473 opbr1st 5501 opbr2nd 5502 funsi 5520 ov3 5599 caovcan 5628 mpt2eq123 5661 ovmpt4g 5710 fnpprod 5843 fnfullfunlem1 5856 extd 5923 antid 5929 qsdisj 5995 ncspw1eu 6159 nchoicelem16 6304 |
Copyright terms: Public domain | W3C validator |