Theorem ifpimpda

Description: Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 27-Feb-2021)

	Ref	Expression
Hypotheses	ifpimpda.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
	ifpimpda.2	$$⊢\left(\phi \wedge \neg \psi \right)\to \theta$$
Assertion	ifpimpda	$$⊢\phi \to if-\left(\psi ,\chi ,\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		ifpimpda.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
2		ifpimpda.2	$$⊢\left(\phi \wedge \neg \psi \right)\to \theta$$
3	1	ex	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	2	ex	$$⊢\phi \to \left(\neg \psi \to \theta \right)$$
5		dfifp2	$$⊢if-\left(\psi ,\chi ,\theta \right)\leftrightarrow \left(\left(\psi \to \chi \right)\wedge \left(\neg \psi \to \theta \right)\right)$$
6	3 4 5	sylanbrc	$$⊢\phi \to if-\left(\psi ,\chi ,\theta \right)$$