This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \land ψ) \to χ$
	ifpimpda.2	$⊢ (φ \land \neg ψ) \to θ$
Assertion	ifpimpda	$⊢ φ \to if- (ψ, χ, θ)$

Proof

Step	Hyp	Ref	Expression
1		ifpimpda.1	$⊢ (φ \land ψ) \to χ$
2		ifpimpda.2	$⊢ (φ \land \neg ψ) \to θ$
3	1	ex	$⊢ φ \to (ψ \to χ)$
4	2	ex	$⊢ φ \to (\neg ψ \to θ)$
5		dfifp2	$⊢ if- (ψ, χ, θ) \leftrightarrow ((ψ \to χ) \land (\neg ψ \to θ))$
6	3 4 5	sylanbrc	$⊢ φ \to if- (ψ, χ, θ)$