![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-mpgs | Structured version Visualization version GIF version |
Description: From a closed form theorem (the major premise) with an antecedent in the "strong necessity" modality (in the language of modal logic), deduce the inference ⊢ 𝜑 ⇒ ⊢ 𝜓. Strong necessity is stronger than necessity, and equivalent to it when sp 2179 (modal T) is available. Therefore, this theorem is stronger than mpg 1792 when sp 2179 is not available. (Contributed by BJ, 1-Nov-2023.) |
Ref | Expression |
---|---|
bj-mpgs.min | ⊢ 𝜑 |
bj-mpgs.maj | ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓) |
Ref | Expression |
---|---|
bj-mpgs | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-mpgs.min | . 2 ⊢ 𝜑 | |
2 | 1 | ax-gen 1790 | . 2 ⊢ ∀𝑥𝜑 |
3 | bj-mpgs.maj | . 2 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∀wal 1533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 |
This theorem depends on definitions: df-bi 207 df-an 396 |
This theorem is referenced by: bj-nnfbii 36670 bj-nnfth 36685 |
Copyright terms: Public domain | W3C validator |