Metamath Proof Explorer

Theorem bj-19.41al

Description: Special case of 19.41 proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-19.41al ⊢ ∃ x φ ∧ ∀ x ψ ↔ ∃ x φ ∧ ∀ x ψ

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ∃ x ∀ x ψ
2 hbe1a ⊢ ∃ x ∀ x ψ → ∀ x ψ
3 2 anim2i ⊢ ∃ x φ ∧ ∃ x ∀ x ψ → ∃ x φ ∧ ∀ x ψ
4 1 3 syl ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ∀ x ψ
5 hba1 ⊢ ∀ x ψ → ∀ x ∀ x ψ
6 5 anim2i ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ∀ x ∀ x ψ
7 19.29r ⊢ ∃ x φ ∧ ∀ x ∀ x ψ → ∃ x φ ∧ ∀ x ψ
8 6 7 syl ⊢ ∃ x φ ∧ ∀ x ψ → ∃ x φ ∧ ∀ x ψ
9 4 8 impbii ⊢ ∃ x φ ∧ ∀ x ψ ↔ ∃ x φ ∧ ∀ x ψ