Metamath Proof Explorer

Theorem ifpdfnan

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

Ref Expression
Assertion ifpdfnan ⊢ φ ⊼ ψ ↔ if- φ ¬ ψ ⊤

Proof

Step Hyp Ref Expression
1 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
2 ifpdfan ⊢ φ ∧ ψ ↔ if- φ ψ ⊥
3 2 notbii ⊢ ¬ φ ∧ ψ ↔ ¬ if- φ ψ ⊥
4 ifpnot23 ⊢ ¬ if- φ ψ ⊥ ↔ if- φ ¬ ψ ¬ ⊥
5 notfal ⊢ ¬ ⊥ ↔ ⊤
6 ifpbi3 ⊢ ¬ ⊥ ↔ ⊤ → if- φ ¬ ψ ¬ ⊥ ↔ if- φ ¬ ψ ⊤
7 5 6 ax-mp ⊢ if- φ ¬ ψ ¬ ⊥ ↔ if- φ ¬ ψ ⊤
8 4 7 bitri ⊢ ¬ if- φ ψ ⊥ ↔ if- φ ¬ ψ ⊤
9 1 3 8 3bitri ⊢ φ ⊼ ψ ↔ if- φ ¬ ψ ⊤