Metamath Proof Explorer

Theorem dfifp3

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

Ref Expression
Assertion dfifp3 ⊢ if- φ ψ χ ↔ φ → ψ ∧ φ ∨ χ

Proof

Step Hyp Ref Expression
1 dfifp2 ⊢ if- φ ψ χ ↔ φ → ψ ∧ ¬ φ → χ
2 pm4.64 ⊢ ¬ φ → χ ↔ φ ∨ χ
3 2 anbi2i ⊢ φ → ψ ∧ ¬ φ → χ ↔ φ → ψ ∧ φ ∨ χ
4 1 3 bitri ⊢ if- φ ψ χ ↔ φ → ψ ∧ φ ∨ χ