Metamath Proof Explorer

Theorem bj-19.21t0

Description: Proof of 19.21t from stdpc5t . (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 stdpc5t ⊢ Ⅎ x φ → ∀ x φ → ψ → φ → ∀ x ψ
2 19.9t ⊢ Ⅎ x φ → ∃ x φ ↔ φ
3 2 imbi1d ⊢ Ⅎ x φ → ∃ x φ → ∀ x ψ ↔ φ → ∀ x ψ
4 19.38 ⊢ ∃ x φ → ∀ x ψ → ∀ x φ → ψ
5 3 4 syl6bir ⊢ Ⅎ x φ → φ → ∀ x ψ → ∀ x φ → ψ
6 1 5 impbid ⊢ Ⅎ x φ → ∀ x φ → ψ ↔ φ → ∀ x ψ