Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > hbc | Unicode version |
Description: Hypothesis builder for combination. |
Ref | Expression |
---|---|
hbc.1 | |
hbc.2 | |
hbc.3 | |
hbc.4 | |
hbc.5 |
Ref | Expression |
---|---|
hbc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbc.1 | . . . . 5 | |
2 | hbc.2 | . . . . 5 | |
3 | 1, 2 | wc 45 | . . . 4 |
4 | 3 | wl 59 | . . 3 |
5 | hbc.3 | . . 3 | |
6 | 4, 5 | wc 45 | . 2 |
7 | hbc.4 | . . . 4 | |
8 | 7 | ax-cb1 29 | . . 3 |
9 | 1, 2, 5 | distrc 83 | . . 3 |
10 | 8, 9 | a1i 28 | . 2 |
11 | 1 | wl 59 | . . . 4 |
12 | 11, 5 | wc 45 | . . 3 |
13 | hbc.5 | . . . 4 | |
14 | 2, 13 | eqtypri 71 | . . 3 |
15 | 12, 14, 7, 13 | ceq12 78 | . 2 |
16 | 6, 10, 15 | eqtri 85 | 1 |
Colors of variables: type var term |
Syntax hints: ht 2 kc 5 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-distrc 61 |
This theorem depends on definitions: df-ov 65 |
This theorem is referenced by: hbov 101 clf 105 exlimdv 157 cbvf 167 leqf 169 exlimd 171 alimdv 172 eximdv 173 alnex 174 exmid 186 ax5 194 ax6 195 ax7 196 ax9 199 axext 206 axrep 207 |
Copyright terms: Public domain | W3C validator |