Theorem impbi

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999)

	Ref	Expression
Assertion	impbi	|- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bi	|- -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2		simprim	|- ( -. ( ( ( ph <-> ps ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) ) -> ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) ) )
3	1 2	ax-mp	|- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ph <-> ps ) )
4	3	expi	|- ( ( ph -> ps ) -> ( ( ps -> ph ) -> ( ph <-> ps ) ) )