![]() |
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 2200 |
. 2
![]() ![]() ![]() ![]() |
4 | 3eqtr3i.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | eqtr3i 2200 |
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 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: csbvarg 3087 un12 3295 in12 3348 indif1 3382 difundir 3390 difindir 3392 dif32 3400 resmpt3 4958 xp0 5050 fvsnun1 5716 caov12 6066 caov13 6068 djuassen 7219 xpdjuen 7220 rec1nq 7397 halfnqq 7412 negsubdii 8245 halfpm6th 9142 decmul1 9450 i4 10626 fac4 10716 imi 10912 resqrexlemover 11022 ef01bndlem 11767 znnen 12402 sn0cld 13798 cospi 14382 sincos4thpi 14422 sincos3rdpi 14425 lgsdir2lem1 14590 lgsdir2lem5 14594 2lgsoddprmlem3d 14619 ex-bc 14642 ex-gcd 14644 |
Copyright terms: Public domain | W3C validator |