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 ⊢φ→ψ↔ψ→φ↔χ↔φ↔ψ∧χ