New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqeq12d | GIF version |
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
eqeq12d.1 | ⊢ (φ → A = B) |
eqeq12d.2 | ⊢ (φ → C = D) |
Ref | Expression |
---|---|
eqeq12d | ⊢ (φ → (A = C ↔ B = D)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq12d.1 | . 2 ⊢ (φ → A = B) | |
2 | eqeq12d.2 | . 2 ⊢ (φ → C = D) | |
3 | eqeq12 2365 | . 2 ⊢ ((A = B ∧ C = D) → (A = C ↔ B = D)) | |
4 | 1, 2, 3 | syl2anc 642 | 1 ⊢ (φ → (A = C ↔ B = D)) |
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-an 360 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: sbceqg 3152 csbing 3462 csbifg 3690 uniprg 3906 unisng 3908 intprg 3960 iununi 4050 csbiotag 4371 preaddccan2 4455 csbopabg 4637 csbima12g 4955 fveqres 5355 eqfnfv2f 5396 fvreseq 5398 fnressn 5438 fvi 5442 fvsng 5446 csbovg 5552 eqfnov 5589 ov2ag 5598 caovcomg 5624 caovassg 5626 caovcan 5628 caovdig 5632 caovdirg 5633 caovmo 5645 ov2gf 5711 fvmptf 5722 fvfullfun 5864 taddc 6228 letc 6230 addcdi 6249 addccan2nc 6264 nchoicelem1 6287 nchoicelem2 6288 nchoicelem9 6295 nchoicelem17 6303 nchoice 6306 |
Copyright terms: Public domain | W3C validator |