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-\left(\phi ,\psi ,\psi \right)\leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		ifptru	$$⊢\phi \to \left(if-\left(\phi ,\psi ,\psi \right)\leftrightarrow \psi \right)$$
2		ifpfal	$$⊢\neg \phi \to \left(if-\left(\phi ,\psi ,\psi \right)\leftrightarrow \psi \right)$$
3	1 2	pm2.61i	$$⊢if-\left(\phi ,\psi ,\psi \right)\leftrightarrow \psi$$