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

Metamath Proof Explorer

Theorem bj-19.21t

Description: Statement 19.21t proved from modalK (obsoleting 19.21v ). (Contributed by BJ, 2-Dec-2023)

Ref Expression
Assertion bj-19.21t ⊢ Ⅎ' x φ → ∀ x φ → ψ ↔ φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 bj-nnf-alrim ⊢ Ⅎ' x φ → ∀ x φ → ψ → φ → ∀ x ψ
2 bj-nnfe ⊢ Ⅎ' x φ → ∃ x φ → φ
3 2 imim1d ⊢ Ⅎ' x φ → φ → ∀ x ψ → ∃ x φ → ∀ x ψ
4 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
5 3 4 syl6 ⊢ Ⅎ' x φ → φ → ∀ x ψ → ∀ x φ → ψ
6 1 5 impbid ⊢ Ⅎ' x φ → ∀ x φ → ψ ↔ φ → ∀ x ψ