Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > adantr | GIF version |
Description: Extract an assumption from the context. |
Ref | Expression |
---|---|
adantr.1 | ⊢ R⊧T |
adantr.2 | ⊢ S:∗ |
Ref | Expression |
---|---|
adantr | ⊢ (R, S)⊧T |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | adantr.1 | . . . 4 ⊢ R⊧T | |
2 | 1 | ax-cb1 29 | . . 3 ⊢ R:∗ |
3 | adantr.2 | . . 3 ⊢ S:∗ | |
4 | 2, 3 | simpl 22 | . 2 ⊢ (R, S)⊧R |
5 | 4, 1 | syl 16 | 1 ⊢ (R, S)⊧T |
Colors of variables: type var term |
Syntax hints: ∗hb 3 kct 10 ⊧wffMMJ2 11 wffMMJ2t 12 |
This theorem was proved from axioms: ax-syl 15 ax-simpl 20 ax-cb1 29 |
This theorem is referenced by: adantl 51 ct1 52 sylan 54 an32s 55 anassrs 57 eqtru 76 hbxfr 98 hbov 101 hbct 145 imp 147 olc 154 orc 155 exlimdv2 156 exlimd 171 ax1 190 ax5 194 ax12 202 ax13 203 ax14 204 |
Copyright terms: Public domain | W3C validator |