![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr3 | Unicode version |
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) |
Ref | Expression |
---|---|
eqtr3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2142 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqtr 2158 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan2b 285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-4 1488 ax-17 1507 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 |
This theorem is referenced by: eueq 2859 euind 2875 reuind 2893 preqsn 3710 eusv1 4381 funopg 5165 funinsn 5180 foco 5363 mpofun 5881 enq0tr 7266 lteupri 7449 elrealeu 7661 rereceu 7721 receuap 8454 xrltso 9612 xrlttri3 9613 iseqf1olemab 10293 fsumparts 11271 odd2np1 11606 exmidsbthrlem 13392 |
Copyright terms: Public domain | W3C validator |