Theorem ifpbiidcor2

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

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

Proof

Step	Hyp	Ref	Expression
1		ifpbiidcor	⊢ if- ( 𝜑 , 𝜑 , ¬ 𝜑 )
2		ifpnot23b	⊢ ( ¬ if- ( 𝜑 , ¬ 𝜑 , 𝜑 ) ↔ if- ( 𝜑 , 𝜑 , ¬ 𝜑 ) )
3	1 2	mpbir	⊢ ¬ if- ( 𝜑 , ¬ 𝜑 , 𝜑 )