Theorem ifptru

Description: Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue . This is essentially dedlema . (Contributed by BJ, 20-Sep-2019) (Proof shortened by Wolf Lammen, 10-Jul-2020)

	Ref	Expression
Assertion	ifptru	$$⊢\phi \to \left(if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		biimt	$$⊢\phi \to \left(\psi \leftrightarrow \left(\phi \to \psi \right)\right)$$
2		orc	$$⊢\phi \to \left(\phi \vee \chi \right)$$
3	2	biantrud	$$⊢\phi \to \left(\left(\phi \to \psi \right)\leftrightarrow \left(\left(\phi \to \psi \right)\wedge \left(\phi \vee \chi \right)\right)\right)$$
4		dfifp3	$$⊢if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi \to \psi \right)\wedge \left(\phi \vee \chi \right)\right)$$
5	3 4	bitr4di	$$⊢\phi \to \left(\left(\phi \to \psi \right)\leftrightarrow if-\left(\phi ,\psi ,\chi \right)\right)$$
6	1 5	bitr2d	$$⊢\phi \to \left(if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \psi \right)$$