New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqtr2i | Unicode version |
Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995.) |
Ref | Expression |
---|---|
eqtr2i.1 | |
eqtr2i.2 |
Ref | Expression |
---|---|
eqtr2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr2i.1 | . . 3 | |
2 | eqtr2i.2 | . . 3 | |
3 | 1, 2 | eqtri 2373 | . 2 |
4 | 3 | eqcomi 2357 | 1 |
Colors of variables: wff setvar class |
Syntax hints: 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: 3eqtrri 2378 3eqtr2ri 2380 dfun3 3493 symdif1 3519 iunin 3547 iinun 3548 dfif3 3672 dfsn2 3747 ssunpr 3868 sstp 3870 tfinnn 4534 xpindi 4864 xpindir 4865 foimacnv 5303 clos1base 5878 pmex 6005 fundmen 6043 nncdiv3 6277 nnc3p1n3p2 6280 nchoicelem1 6289 |
Copyright terms: Public domain | W3C validator |