Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr2i | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) |
Ref | Expression |
---|---|
3eqtr2i.1 | |
3eqtr2i.2 | |
3eqtr2i.3 |
Ref | Expression |
---|---|
3eqtr2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr2i.1 | . . 3 | |
2 | 3eqtr2i.2 | . . 3 | |
3 | 1, 2 | eqtr4i 2189 | . 2 |
4 | 3eqtr2i.3 | . 2 | |
5 | 3, 4 | eqtri 2186 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1343 |
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 1435 ax-gen 1437 ax-4 1498 ax-17 1514 ax-ext 2147 |
This theorem depends on definitions: df-bi 116 df-cleq 2158 |
This theorem is referenced by: dfrab3 3398 iunid 3921 cnvcnv 5056 cocnvcnv2 5115 fmptap 5675 exmidfodomrlemim 7157 negdii 8182 halfpm6th 9077 numma 9365 numaddc 9369 6p5lem 9391 8p2e10 9401 binom2i 10563 0.999... 11462 flodddiv4 11871 6gcd4e2 11928 dfphi2 12152 txswaphmeolem 12960 cosq23lt0 13394 pigt3 13405 nninfomni 13899 |
Copyright terms: Public domain | W3C validator |