Theorem bj-mpgs 34718

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 2178 (modal T) is available. Therefore, this theorem is stronger than mpg 1801 when sp 2178 is not available. (Contributed by BJ, 1-Nov-2023.)

Hypotheses

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

Assertion

Ref	Expression
bj-mpgs	⊢ 𝜓

Proof of Theorem bj-mpgs

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537

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

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  bj-nnfbii  34836  bj-nnfth  34851