Theorem anifp

Description: The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor . (Contributed by BJ, 30-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		olc	$$⊢\psi \to \left(\neg \phi \vee \psi \right)$$
2		olc	$$⊢\chi \to \left(\phi \vee \chi \right)$$
3	1 2	anim12i	$$⊢\left(\psi \wedge \chi \right)\to \left(\left(\neg \phi \vee \psi \right)\wedge \left(\phi \vee \chi \right)\right)$$
4		dfifp4	$$⊢if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\neg \phi \vee \psi \right)\wedge \left(\phi \vee \chi \right)\right)$$
5	3 4	sylibr	$$⊢\left(\psi \wedge \chi \right)\to if-\left(\phi ,\psi ,\chi \right)$$