Theorem ifpbiidcor

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

	Ref	Expression
Assertion	ifpbiidcor	⊢ if- ( 𝜑 , 𝜑 , ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( 𝜑 ↔ 𝜑 )
2		ifpdfbi	⊢ ( ( 𝜑 ↔ 𝜑 ) ↔ if- ( 𝜑 , 𝜑 , ¬ 𝜑 ) )
3	1 2	mpbi	⊢ if- ( 𝜑 , 𝜑 , ¬ 𝜑 )