Theorem ifpbiidcor

Description: Restatement of biid . (Contributed by RP, 25-Apr-2020)

	Ref	Expression
Assertion	ifpbiidcor	|- if- ( ph , ph , -. ph )

Proof

Step	Hyp	Ref	Expression
1		biid	|- ( ph <-> ph )
2		ifpdfbi	|- ( ( ph <-> ph ) <-> if- ( ph , ph , -. ph ) )
3	1 2	mpbi	|- if- ( ph , ph , -. ph )