Metamath Proof Explorer

Theorem biadan

Description: An implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction. A utility lemma as illustrated in biadanii and elelb . (Contributed by BJ, 4-Mar-2023) (Proof shortened by Wolf Lammen, 8-Mar-2023)

Ref Expression
Assertion biadan ⊢ φ → ψ ↔ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 pm4.71r ⊢ φ → ψ ↔ φ ↔ ψ ∧ φ
2 bicom ⊢ φ ↔ ψ ∧ φ ↔ ψ ∧ φ ↔ φ
3 bicom ⊢ φ ↔ ψ ∧ χ ↔ ψ ∧ χ ↔ φ
4 pm5.32 ⊢ ψ → φ ↔ χ ↔ ψ ∧ φ ↔ ψ ∧ χ
5 3 4 bibi12i ⊢ φ ↔ ψ ∧ χ ↔ ψ → φ ↔ χ ↔ ψ ∧ χ ↔ φ ↔ ψ ∧ φ ↔ ψ ∧ χ
6 bicom ⊢ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ ↔ φ ↔ ψ ∧ χ ↔ ψ → φ ↔ χ
7 biluk ⊢ ψ ∧ φ ↔ φ ↔ ψ ∧ χ ↔ φ ↔ ψ ∧ φ ↔ ψ ∧ χ
8 5 6 7 3bitr4ri ⊢ ψ ∧ φ ↔ φ ↔ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ
9 1 2 8 3bitri ⊢ φ → ψ ↔ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ