Description: Obsolete version of nfnbi as of 6-Oct-2024. (Contributed by BJ, 6-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfnbiOLD | ⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 ¬ 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | orcom | ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) ) | |
| 2 | nf3 | ⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) ) | |
| 3 | nf3 | ⊢ ( Ⅎ 𝑥 ¬ 𝜑 ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 ¬ ¬ 𝜑 ) ) | |
| 4 | notnotb | ⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 ) | |
| 5 | 4 | albii | ⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ ¬ 𝜑 ) |
| 6 | 5 | orbi2i | ⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 ¬ ¬ 𝜑 ) ) |
| 7 | 3 6 | bitr4i | ⊢ ( Ⅎ 𝑥 ¬ 𝜑 ↔ ( ∀ 𝑥 ¬ 𝜑 ∨ ∀ 𝑥 𝜑 ) ) |
| 8 | 1 2 7 | 3bitr4i | ⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 ¬ 𝜑 ) |