Theorem abab

Description: Introduce one conjunct as equivalent to the other. "abab" stands for "and, biconditional, and, biconditional". (Contributed by Wolf Lammen, 4-Jun-2026)

	Ref	Expression
Assertion	abab	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝜑 ↔ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
2		pm5.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ↔ 𝜓 ) )
3	1 2	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ( 𝜑 ↔ 𝜓 ) ) )
4		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
5	4	anim2i	⊢ ( ( 𝜑 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) )
6		abai	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) )
7	5 6	sylibr	⊢ ( ( 𝜑 ∧ ( 𝜑 ↔ 𝜓 ) ) → ( 𝜑 ∧ 𝜓 ) )
8	3 7	impbii	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ( 𝜑 ↔ 𝜓 ) ) )