Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > mpbi | GIF version |
Description: Deduction from equality inference. |
Ref | Expression |
---|---|
mpbi.1 | ⊢ R⊧A |
mpbi.2 | ⊢ R⊧[A = B] |
Ref | Expression |
---|---|
mpbi | ⊢ R⊧B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbi.1 | . 2 ⊢ R⊧A | |
2 | weq 38 | . . 3 ⊢ = :(∗ → (∗ → ∗)) | |
3 | 1 | ax-cb2 30 | . . 3 ⊢ A:∗ |
4 | mpbi.2 | . . . 4 ⊢ R⊧[A = B] | |
5 | 3, 4 | eqtypi 69 | . . 3 ⊢ B:∗ |
6 | 2, 3, 5, 4 | dfov1 66 | . 2 ⊢ R⊧(( = A)B) |
7 | 1, 6 | ax-eqmp 42 | 1 ⊢ R⊧B |
Colors of variables: type var term |
Syntax hints: ∗hb 3 = ke 7 [kbr 9 ⊧wffMMJ2 11 |
This theorem was proved from axioms: ax-syl 15 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-eqmp 42 |
This theorem depends on definitions: df-ov 65 |
This theorem is referenced by: mpbir 77 eqtri 85 ax4g 139 ax4 140 cla4v 142 pm2.21 143 dfan2 144 mpd 146 notval2 149 notnot1 150 con2d 151 ecase 153 exlimdv2 156 exlimd 171 alnex 174 exnal1 175 exmid 186 notnot 187 ax3 192 ax11 201 ax13 203 ax14 204 |
Copyright terms: Public domain | W3C validator |