Metamath Proof Explorer

Theorem alsbid

Description: Deduction form of alsbii . (Contributed by David A. Wheeler, 12-Jul-2026)

Ref Expression
Hypotheses alsbid.1 ⊢ Ⅎ x φ
alsbid.2 ⊢ φ → ψ ↔ θ
alsbid.3 ⊢ φ → χ ↔ τ
Assertion alsbid ⊢ φ → ∀∃ x ψ → χ ↔ ∀∃ x θ → τ

Proof

Step Hyp Ref Expression
1 alsbid.1 ⊢ Ⅎ x φ
2 alsbid.2 ⊢ φ → ψ ↔ θ
3 alsbid.3 ⊢ φ → χ ↔ τ
4 2 3 imbi12d ⊢ φ → ψ → χ ↔ θ → τ
5 1 4 albid ⊢ φ → ∀ x ψ → χ ↔ ∀ x θ → τ
6 1 2 exbid ⊢ φ → ∃ x ψ ↔ ∃ x θ
7 5 6 anbi12d ⊢ φ → ∀ x ψ → χ ∧ ∃ x ψ ↔ ∀ x θ → τ ∧ ∃ x θ
8 df-als ⊢ ∀∃ x ψ → χ ↔ ∀ x ψ → χ ∧ ∃ x ψ
9 df-als ⊢ ∀∃ x θ → τ ↔ ∀ x θ → τ ∧ ∃ x θ
10 7 8 9 3bitr4g ⊢ φ → ∀∃ x ψ → χ ↔ ∀∃ x θ → τ