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 2194 | . 2 |
4 | 3eqtr2i.3 | . 2 | |
5 | 3, 4 | eqtri 2191 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: dfrab3 3403 iunid 3926 cnvcnv 5061 cocnvcnv2 5120 fmptap 5683 exmidfodomrlemim 7165 negdii 8190 halfpm6th 9085 numma 9373 numaddc 9377 6p5lem 9399 8p2e10 9409 binom2i 10571 0.999... 11471 flodddiv4 11880 6gcd4e2 11937 dfphi2 12161 txswaphmeolem 13035 cosq23lt0 13469 pigt3 13480 nninfomni 13974 |
Copyright terms: Public domain | W3C validator |