![]() |
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 | eqtrdi 2238 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4a.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr4d 2225 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: uniintsnr 3895 fndmdifcom 5638 offres 6154 1stval2 6174 2ndval2 6175 ecovcom 6660 ecovass 6662 ecovdi 6664 nnnninfeq2 7145 zeo 9376 xnegneg 9851 xaddcom 9879 xaddid1 9880 xnegdi 9886 fzsuc2 10097 expnegap0 10546 facp1 10728 bcpasc 10764 hashfzp1 10822 resunimafz0 10829 absexp 11106 iooinsup 11303 fsumf1o 11416 fsumadd 11432 fisumrev2 11472 fsumparts 11496 fprodf1o 11614 fprodmul 11617 efexp 11708 tanval2ap 11739 gcdcom 11992 gcd0id 11998 dfgcd3 12029 gcdass 12034 lcmcom 12082 lcmneg 12092 lcmass 12103 sqrt2irrlem 12179 nn0gcdsq 12218 dfphi2 12238 eulerthlemth 12250 pcneg 12342 setscom 12520 restco 14071 txtopon 14159 dvef 14585 lgsneg 14822 lgsneg1 14823 lgsdir2 14831 lgsdir 14833 lgsdi 14835 |
Copyright terms: Public domain | W3C validator |