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 2140 | . 2 |
4 | 3eqtr3i.3 | . 2 | |
5 | 3, 4 | eqtr3i 2140 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 |
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 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: csbvarg 3000 un12 3204 in12 3257 indif1 3291 difundir 3299 difindir 3301 dif32 3309 resmpt3 4838 xp0 4928 fvsnun1 5585 caov12 5927 caov13 5929 djuassen 7041 xpdjuen 7042 rec1nq 7171 halfnqq 7186 negsubdii 8015 halfpm6th 8908 decmul1 9213 i4 10363 fac4 10447 imi 10640 resqrexlemover 10750 ef01bndlem 11390 znnen 11838 sn0cld 12233 cospi 12808 sincos4thpi 12848 sincos3rdpi 12851 ex-bc 12868 ex-gcd 12870 |
Copyright terms: Public domain | W3C validator |