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 φψχ
ifpimpda.2 φ¬ψθ
Assertion ifpimpda φif-ψχθ

Proof

Step Hyp Ref Expression
1 ifpimpda.1 φψχ
2 ifpimpda.2 φ¬ψθ
3 1 ex φψχ
4 2 ex φ¬ψθ
5 dfifp2 if-ψχθψχ¬ψθ
6 3 4 5 sylanbrc φif-ψχθ