Metamath Proof Explorer


Theorem dfifp3

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

Ref Expression
Assertion dfifp3 if-φψχφψφχ

Proof

Step Hyp Ref Expression
1 dfifp2 if-φψχφψ¬φχ
2 pm4.64 ¬φχφχ
3 2 anbi2i φψ¬φχφψφχ
4 1 3 bitri if-φψχφψφχ