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 2188 | . 2 |
4 | 3eqtr2i.3 | . 2 | |
5 | 3, 4 | eqtri 2185 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: dfrab3 3393 iunid 3915 cnvcnv 5050 cocnvcnv2 5109 fmptap 5669 exmidfodomrlemim 7148 negdii 8173 halfpm6th 9068 numma 9356 numaddc 9360 6p5lem 9382 8p2e10 9392 binom2i 10553 0.999... 11448 flodddiv4 11856 6gcd4e2 11913 dfphi2 12131 txswaphmeolem 12867 cosq23lt0 13301 pigt3 13312 nninfomni 13740 |
Copyright terms: Public domain | W3C validator |