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 2 anbi1i ⊢ φ → ψ ∧ ¬ φ → χ ↔ ¬ φ ∨ ψ ∧ ¬ φ → χ
4 1 3 bitri ⊢ if- φ ψ χ ↔ ¬ φ ∨ ψ ∧ ¬ φ → χ