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-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-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 6229 letc 6231 addcdi 6250 addccan2nc 6265 nchoicelem1 6289 nchoicelem2 6290 nchoicelem9 6297 nchoicelem17 6305 nchoice 6308 |
Copyright terms: Public domain | W3C validator |