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- ( ph , ps , ps ) <-> ps )

Proof

Step	Hyp	Ref	Expression
1		ifptru	|- ( ph -> ( if- ( ph , ps , ps ) <-> ps ) )
2		ifpfal	|- ( -. ph -> ( if- ( ph , ps , ps ) <-> ps ) )
3	1 2	pm2.61i	|- ( if- ( ph , ps , ps ) <-> ps )