Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > eqtri | Unicode version |
Description: Transitivity of equality. |
Ref | Expression |
---|---|
eqtri.1 | |
eqtri.2 | |
eqtri.3 |
Ref | Expression |
---|---|
eqtri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weq 38 | . 2 | |
2 | eqtri.1 | . 2 | |
3 | eqtri.2 | . . . 4 | |
4 | 2, 3 | eqtypi 69 | . . 3 |
5 | eqtri.3 | . . 3 | |
6 | 4, 5 | eqtypi 69 | . 2 |
7 | 1, 2, 4, 3 | dfov1 66 | . . 3 |
8 | 1, 2 | wc 45 | . . . 4 |
9 | 8, 4, 5 | ceq2 80 | . . 3 |
10 | 7, 9 | mpbi 72 | . 2 |
11 | 1, 2, 6, 10 | dfov2 67 | 1 |
Colors of variables: type var term |
Syntax hints: ht 2 hb 3 kc 5 ke 7 kbr 9 wffMMJ2 11 wffMMJ2t 12 |
This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ceq 46 |
This theorem depends on definitions: df-ov 65 |
This theorem is referenced by: 3eqtr4i 86 hbc 100 hbl 102 ovl 107 alval 132 exval 133 euval 134 notval 135 imval 136 orval 137 anval 138 ax4g 139 dfan2 144 ex 148 notval2 149 olc 154 orc 155 exlimdv 157 cbvf 167 exlimd 171 exmid 186 ax8 198 ax10 200 ax11 201 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |