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	|- ( ( ph /\ ps ) -> ch )
	ifpimpda.2	|- ( ( ph /\ -. ps ) -> th )
Assertion	ifpimpda	|- ( ph -> if- ( ps , ch , th ) )

Proof

Step	Hyp	Ref	Expression
1		ifpimpda.1	|- ( ( ph /\ ps ) -> ch )
2		ifpimpda.2	|- ( ( ph /\ -. ps ) -> th )
3	1	ex	|- ( ph -> ( ps -> ch ) )
4	2	ex	|- ( ph -> ( -. ps -> th ) )
5		dfifp2	|- ( if- ( ps , ch , th ) <-> ( ( ps -> ch ) /\ ( -. ps -> th ) ) )
6	3 4 5	sylanbrc	|- ( ph -> if- ( ps , ch , th ) )