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	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( ( 𝜓 → ( 𝜑 ↔ 𝜒 ) ) ↔ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) ) ) )