This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-mpgs

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

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

Proof

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