Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > leq | Unicode version |
Description: Equality theorem for lambda abstraction. |
Ref | Expression |
---|---|
leq.1 | |
leq.2 |
Ref | Expression |
---|---|
leq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weq 38 | . 2 | |
2 | leq.1 | . . 3 | |
3 | 2 | wl 59 | . 2 |
4 | leq.2 | . . . 4 | |
5 | 2, 4 | eqtypi 69 | . . 3 |
6 | 5 | wl 59 | . 2 |
7 | weq 38 | . . . 4 | |
8 | 7, 2, 5, 4 | dfov1 66 | . . 3 |
9 | 2, 5, 8 | ax-leq 62 | . 2 |
10 | 1, 3, 6, 9 | dfov2 67 | 1 |
Colors of variables: type var term |
Syntax hints: ht 2 kl 6 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 ax-leq 62 |
This theorem depends on definitions: df-ov 65 |
This theorem is referenced by: hbxfrf 97 hbl 102 exval 133 euval 134 orval 137 anval 138 alrimiv 141 dfan2 144 olc 154 orc 155 exlimdv2 156 eta 166 cbvf 167 leqf 169 exlimd 171 ac 184 exmid 186 exnal 188 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |