Theorem bj-bibibi

Description: A property of the biconditional. (Contributed by BJ, 26-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-bibibi	|- ( ph <-> ( ps <-> ( ph <-> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm5.501	|- ( ph -> ( ps <-> ( ph <-> ps ) ) )
2		bianir	|- ( ( ps /\ ( ph <-> ps ) ) -> ph )
3	2	ex	|- ( ps -> ( ( ph <-> ps ) -> ph ) )
4		bibif	|- ( -. ps -> ( ( ph <-> ps ) <-> -. ph ) )
5	4	con2bid	|- ( -. ps -> ( ph <-> -. ( ph <-> ps ) ) )
6	5	biimprd	|- ( -. ps -> ( -. ( ph <-> ps ) -> ph ) )
7	3 6	bija	|- ( ( ps <-> ( ph <-> ps ) ) -> ph )
8	1 7	impbii	|- ( ph <-> ( ps <-> ( ph <-> ps ) ) )