Metamath Proof Explorer


Theorem ifpim3

Description: Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpim3 φψif-φψ¬φ

Proof

Step Hyp Ref Expression
1 simpl φψφ
2 orc φφψ
3 ifpim23g φψif-φψ¬φφψφφφψ
4 1 2 3 mpbir2an φψif-φψ¬φ