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

Metamath Proof Explorer

Theorem bj-nnf-alrim

Description: Proof of the closed form of alrimi from modalK (compare alrimiv ). See also bj-alrim . Actually, most proofs between 19.3t and 2sbbid could be proved without ax-12 . (Contributed by BJ, 20-Aug-2023)

		Ref	Expression
	Assertion	bj-nnf-alrim	⊢ ( Ⅎ' 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnfa	⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
2		alim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
3	1 2	syl9	⊢ ( Ⅎ' 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) ) )