Metamath Proof Explorer

Theorem ifpnot

Description: Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpnot ⊢ ¬ φ ↔ if- φ ⊥ ⊤

Proof

Step Hyp Ref Expression
1 tru ⊢ ⊤
2 1 olci ⊢ φ ∨ ⊤
3 2 biantru ⊢ ¬ φ ∨ ⊥ ↔ ¬ φ ∨ ⊥ ∧ φ ∨ ⊤
4 fal ⊢ ¬ ⊥
5 4 biorfri ⊢ ¬ φ ↔ ¬ φ ∨ ⊥
6 dfifp4 ⊢ if- φ ⊥ ⊤ ↔ ¬ φ ∨ ⊥ ∧ φ ∨ ⊤
7 3 5 6 3bitr4i ⊢ ¬ φ ↔ if- φ ⊥ ⊤