Metamath Proof Explorer

Theorem ifpdfor

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

Ref Expression
Assertion ifpdfor φ ψ if- φ ψ


Step Hyp Ref Expression
1 tru
2 1 olci ¬ φ
3 2 biantrur φ ψ ¬ φ φ ψ
4 dfifp4 if- φ ψ ¬ φ φ ψ
5 3 4 bitr4i φ ψ if- φ ψ