![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3i | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr3i.1 |
![]() ![]() ![]() ![]() |
3eqtr3i.2 |
![]() ![]() ![]() ![]() |
3eqtr3i.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr3i |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr3i.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqtr3i 2111 |
. 2
![]() ![]() ![]() ![]() |
4 | 3eqtr3i.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr3i 2111 |
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: csbvarg 2959 un12 3159 in12 3212 indif1 3245 difundir 3253 difindir 3255 dif32 3263 resmpt3 4774 xp0 4864 fvsnun1 5508 caov12 5847 caov13 5849 rec1nq 7015 halfnqq 7030 negsubdii 7828 halfpm6th 8697 decmul1 9001 i4 10118 fac4 10202 imi 10395 resqrexlemover 10504 ef01bndlem 11108 znnen 11550 sn0cld 11898 ex-bc 11929 ex-gcd 11931 |
Copyright terms: Public domain | W3C validator |