Theorem 1fpid3

Description: The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021)

	Ref	Expression
Hypothesis	1fpid3.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
Assertion	1fpid3	$$⊢if-\left(\phi ,\psi ,\chi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		1fpid3.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
2		df-ifp	$$⊢if-\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \chi \right)\right)$$
3		simpr	$$⊢\left(\neg \phi \wedge \chi \right)\to \chi$$
4	1 3	jaoi	$$⊢\left(\left(\phi \wedge \psi \right)\vee \left(\neg \phi \wedge \chi \right)\right)\to \chi$$
5	2 4	sylbi	$$⊢if-\left(\phi ,\psi ,\chi \right)\to \chi$$