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	|- ( ( ph /\ ps ) <-> ( ph /\ ( ph <-> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ph /\ ps ) -> ph )
2		pm5.1	|- ( ( ph /\ ps ) -> ( ph <-> ps ) )
3	1 2	jca	|- ( ( ph /\ ps ) -> ( ph /\ ( ph <-> ps ) ) )
4		biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )
5	4	anim2i	|- ( ( ph /\ ( ph <-> ps ) ) -> ( ph /\ ( ph -> ps ) ) )
6		abai	|- ( ( ph /\ ps ) <-> ( ph /\ ( ph -> ps ) ) )
7	5 6	sylibr	|- ( ( ph /\ ( ph <-> ps ) ) -> ( ph /\ ps ) )
8	3 7	impbii	|- ( ( ph /\ ps ) <-> ( ph /\ ( ph <-> ps ) ) )