![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4a | Unicode version |
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4a.1 |
![]() ![]() ![]() ![]() |
3eqtr4a.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4a.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4a.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr4a.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6eq 2137 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4a.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr4d 2124 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-4 1446 ax-17 1465 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 |
This theorem is referenced by: uniintsnr 3732 fndmdifcom 5421 offres 5922 1stval2 5942 2ndval2 5943 ecovcom 6415 ecovass 6417 ecovdi 6419 zeo 8914 xnegneg 9358 fzsuc2 9556 expnegap0 10026 facp1 10201 bcpasc 10237 hashfzp1 10295 resunimafz0 10299 absexp 10575 fsumf1o 10845 fsumadd 10863 fisumrev2 10903 fsumparts 10927 efexp 11035 tanval2ap 11067 gcdcom 11306 gcd0id 11311 dfgcd3 11340 gcdass 11345 lcmcom 11387 lcmneg 11397 lcmass 11408 sqrt2irrlem 11481 nn0gcdsq 11519 dfphi2 11537 setscom 11597 |
Copyright terms: Public domain | W3C validator |