Metamath Proof Explorer


Theorem ifpdfor2

Description: Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpdfor2 φ ψ if- φ φ ψ

Proof

Step Hyp Ref Expression
1 pm2.1 ¬ φ φ
2 1 biantrur φ ψ ¬ φ φ φ ψ
3 dfifp4 if- φ φ ψ ¬ φ φ φ ψ
4 2 3 bitr4i φ ψ if- φ φ ψ