Theorem ifpid

Description: Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid . This is essentially pm4.42 . (Contributed by BJ, 20-Sep-2019)

	Ref	Expression
Assertion	ifpid	⊢ ( if- ( 𝜑 , 𝜓 , 𝜓 ) ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ifptru	⊢ ( 𝜑 → ( if- ( 𝜑 , 𝜓 , 𝜓 ) ↔ 𝜓 ) )
2		ifpfal	⊢ ( ¬ 𝜑 → ( if- ( 𝜑 , 𝜓 , 𝜓 ) ↔ 𝜓 ) )
3	1 2	pm2.61i	⊢ ( if- ( 𝜑 , 𝜓 , 𝜓 ) ↔ 𝜓 )