Metamath Proof Explorer


Theorem dfifp5

Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)

Ref Expression
Assertion dfifp5 if-φψχ¬φψ¬φχ

Proof

Step Hyp Ref Expression
1 dfifp2 if-φψχφψ¬φχ
2 imor φψ¬φψ
3 1 2 bianbi if-φψχ¬φψ¬φχ