Metamath Proof Explorer

Theorem ifpnot23

Description: Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∨ ¬ ψ
2 pm4.55 ⊢ ¬ ¬ φ ∧ χ ↔ φ ∨ ¬ χ
3 1 2 anbi12i ⊢ ¬ φ ∧ ψ ∧ ¬ ¬ φ ∧ χ ↔ ¬ φ ∨ ¬ ψ ∧ φ ∨ ¬ χ
4 ioran ⊢ ¬ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ ¬ φ ∧ ψ ∧ ¬ ¬ φ ∧ χ
5 dfifp4 ⊢ if- φ ¬ ψ ¬ χ ↔ ¬ φ ∨ ¬ ψ ∧ φ ∨ ¬ χ
6 3 4 5 3bitr4i ⊢ ¬ φ ∧ ψ ∨ ¬ φ ∧ χ ↔ if- φ ¬ ψ ¬ χ
7 df-ifp ⊢ if- φ ψ χ ↔ φ ∧ ψ ∨ ¬ φ ∧ χ
8 6 7 xchnxbir ⊢ ¬ if- φ ψ χ ↔ if- φ ¬ ψ ¬ χ