Theorem bj-bibibi 32571

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

Assertion

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

Proof of Theorem bj-bibibi

Step	Hyp	Ref	Expression
1		pm5.501 356	. 2 |- ( ph -> ( ps <-> ( ph <-> ps ) ) )
2		bianir 1009	. . . 4 |- ( ( ps /\ ( ph <-> ps ) ) -> ph )
3	2	ex 450	. . 3 |- ( ps -> ( ( ph <-> ps ) -> ph ) )
4		bibif 361	. . . . 5 |- ( -. ps -> ( ( ph <-> ps ) <-> -. ph ) )
5	4	con2bid 344	. . . 4 |- ( -. ps -> ( ph <-> -. ( ph <-> ps ) ) )
6	5	biimprd 238	. . 3 |- ( -. ps -> ( -. ( ph <-> ps ) -> ph ) )
7	3, 6	bija 370	. 2 |- ( ( ps <-> ( ph <-> ps ) ) -> ph )
8	1, 7	impbii 199	1 |- ( ph <-> ( ps <-> ( ph <-> ps ) ) )

Syntax hints:   -. wn 3   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by: (None)