Theorem bj-mpgs 37313

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 2221 (modal T) is available. Therefore, this theorem is stronger than mpg 1830, and strictly stronger when sp 2221 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 1828	. 2 ⊢ ∀𝑥𝜑
3		bj-mpgs.maj	. 2 ⊢ ((𝜑 ∧ ∀𝑥𝜑) → 𝜓)
4	1, 2, 3	mp2an 705	1 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bj-nnfth  37479  bj-nnfbii  37484