![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3a | Unicode version |
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
3eqtr3a.1 |
![]() ![]() ![]() ![]() |
3eqtr3a.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr3a.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr3a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3a.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr3a.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 3eqtr3a.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtrid 2232 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtr3d 2222 |
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 1457 ax-gen 1459 ax-4 1520 ax-17 1536 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-cleq 2180 |
This theorem is referenced by: uneqin 3398 coi2 5157 foima 5455 f1imacnv 5490 fvsnun2 5727 fnsnsplitdc 6520 phplem4 6869 phplem4on 6881 halfnqq 7423 resqrexlemcalc1 11037 absefib 11792 efieq1re 11793 restopnb 14034 cnmpt2t 14146 reeflog 14637 rpcxpsqrt 14695 |
Copyright terms: Public domain | W3C validator |