Metamath Proof Explorer

Theorem dfifp6

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

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

Proof

Step Hyp Ref Expression
1 df-ifp ⊢ if- φ ψ χ ↔ φ ∧ ψ ∨ ¬ φ ∧ χ
2 ancom ⊢ ¬ φ ∧ χ ↔ χ ∧ ¬ φ
3 annim ⊢ χ ∧ ¬ φ ↔ ¬ χ → φ
4 2 3 bitri ⊢ ¬ φ ∧ χ ↔ ¬ χ → φ
5 4 orbi2i ⊢ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ φ ∧ ψ ∨ ¬ χ → φ
6 1 5 bitri ⊢ if- φ ψ χ ↔ φ ∧ ψ ∨ ¬ χ → φ