Theorem bj-mpgs 36922

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 associated inference. Strong necessity is stronger than necessity, and equivalent to it when sp 2195 (modal T) is available. Therefore, this theorem is stronger than mpg 1804, and strictly stronger when sp 2195 is not available. (Contributed by BJ, 1-Nov-2023.)

Hypotheses

Ref	Expression
bj-mpgs.maj	⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)
bj-mpgs.min	⊢ 𝜑

Assertion

Ref	Expression
bj-mpgs	⊢ 𝜓

Proof of Theorem bj-mpgs

Step	Hyp	Ref	Expression
1		bj-mpgs.min	. 2 ⊢ 𝜑
2	1	ax-gen 1802	. 2 ⊢ ∀𝑥𝜑
3		bj-mpgs.maj	. 2 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)
4	1, 2, 3	mp2an 698	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  bj-nnfth  37088  bj-nnfbii  37093