Metamath Proof Explorer

Theorem ifpn

Description: Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019) (Proof shortened by Wolf Lammen, 5-May-2024)

Ref Expression
Assertion ifpn ⊢ if- φ ψ χ ↔ if- ¬ φ χ ψ

Proof

Step Hyp Ref Expression
1 ancom ⊢ ¬ φ ∨ ψ ∧ ¬ φ → χ ↔ ¬ φ → χ ∧ ¬ φ ∨ ψ
2 dfifp5 ⊢ if- φ ψ χ ↔ ¬ φ ∨ ψ ∧ ¬ φ → χ
3 dfifp3 ⊢ if- ¬ φ χ ψ ↔ ¬ φ → χ ∧ ¬ φ ∨ ψ
4 1 2 3 3bitr4i ⊢ if- φ ψ χ ↔ if- ¬ φ χ ψ