Metamath Proof Explorer

Theorem ifpid2

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

Ref Expression
Assertion ifpid2 ⊢ φ ↔ if- φ ⊤ ⊥

Proof

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