Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ex | Unicode version |
Description: Exportation deduction. |
Ref | Expression |
---|---|
ex.1 |
Ref | Expression |
---|---|
ex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wan 126 | . . . 4 | |
2 | ex.1 | . . . . . 6 | |
3 | 2 | ax-cb1 29 | . . . . 5 |
4 | 3 | wctr 32 | . . . 4 |
5 | 2 | ax-cb2 30 | . . . 4 |
6 | 1, 4, 5 | wov 64 | . . 3 |
7 | 3 | wctl 31 | . . . 4 |
8 | 4, 5 | dfan2 144 | . . . 4 |
9 | 7, 8 | a1i 28 | . . 3 |
10 | 4, 5 | wct 44 | . . . . . 6 |
11 | 7, 10 | simpr 23 | . . . . 5 |
12 | 11 | simpld 35 | . . . 4 |
13 | 7, 4 | simpr 23 | . . . . 5 |
14 | 13, 2 | jca 18 | . . . 4 |
15 | 12, 14 | ded 74 | . . 3 |
16 | 6, 9, 15 | eqtri 85 | . 2 |
17 | 16 | ax-cb1 29 | . . 3 |
18 | 4, 5 | imval 136 | . . 3 |
19 | 17, 18 | a1i 28 | . 2 |
20 | 16, 19 | mpbir 77 | 1 |
Colors of variables: type var term |
Syntax hints: hb 3 ke 7 kbr 9 kct 10 wffMMJ2 11 tan 109 tim 111 |
This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-simpl 20 ax-simpr 21 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ded 43 ax-ceq 46 ax-beta 60 ax-distrc 61 ax-leq 62 ax-distrl 63 ax-hbl1 93 ax-17 95 ax-inst 103 |
This theorem depends on definitions: df-ov 65 df-an 118 df-im 119 |
This theorem is referenced by: notval2 149 notnot1 150 con2d 151 ecase 153 olc 154 orc 155 exlimdv2 156 exlimdv 157 ax4e 158 exlimd 171 alnex 174 isfree 176 exmid 186 ax1 190 ax2 191 ax3 192 ax5 194 ax7 196 ax8 198 ax10 200 ax11 201 ax12 202 ax13 203 ax14 204 axext 206 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |