Metamath Proof Explorer

Theorem dfifp4

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

Ref Expression
Assertion dfifp4 ⊢ if- φ ψ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ

Proof

Step Hyp Ref Expression
1 dfifp3 ⊢ if- φ ψ χ ↔ φ → ψ ∧ φ ∨ χ
2 imor ⊢ φ → ψ ↔ ¬ φ ∨ ψ
3 2 anbi1i ⊢ φ → ψ ∧ φ ∨ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ
4 1 3 bitri ⊢ if- φ ψ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ