New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqtr4d | GIF version |
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |
Ref | Expression |
---|---|
eqtr4d.1 | ⊢ (φ → A = B) |
eqtr4d.2 | ⊢ (φ → C = B) |
Ref | Expression |
---|---|
eqtr4d | ⊢ (φ → A = C) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4d.1 | . 2 ⊢ (φ → A = B) | |
2 | eqtr4d.2 | . . 3 ⊢ (φ → C = B) | |
3 | 2 | eqcomd 2358 | . 2 ⊢ (φ → B = C) |
4 | 1, 3 | eqtrd 2385 | 1 ⊢ (φ → A = C) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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: 3eqtr2d 2391 3eqtr2rd 2392 3eqtr4d 2395 3eqtr4rd 2396 3eqtr4a 2411 sbnfc2 3196 ifsb 3671 ifeq1da 3687 ifeq2da 3688 ifnot 3700 ifan 3701 ifor 3702 setswith 4321 iotauni 4351 dfiota3 4370 dfiota4 4372 nnsucelrlem3 4426 nnpw1ex 4484 tfin11 4493 sfin112 4529 fveqres 5355 funfv 5375 fsn2 5434 fvunsn 5444 fconst2g 5452 ndmovcom 5617 ndmovass 5618 ndmovdistr 5619 fvmpti 5699 fvmptex 5721 fvfullfun 5864 uniqs2 5985 enprmaplem3 6078 nchoicelem7 6295 nchoicelem15 6303 nchoicelem17 6305 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |