Metamath Proof Explorer

Theorem sbnfOLD

Description: Obsolete version of sbnf as of 2-May-2025. (Contributed by BJ, 2-May-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbnfOLD ⊢ z y Ⅎ x φ ↔ Ⅎ x z y φ

Proof

Step Hyp Ref Expression
1 sbim ⊢ z y φ → ∀ x φ ↔ z y φ → z y ∀ x φ
2 sbal ⊢ z y ∀ x φ ↔ ∀ x z y φ
3 2 imbi2i ⊢ z y φ → z y ∀ x φ ↔ z y φ → ∀ x z y φ
4 1 3 bitri ⊢ z y φ → ∀ x φ ↔ z y φ → ∀ x z y φ
5 4 albii ⊢ ∀ x z y φ → ∀ x φ ↔ ∀ x z y φ → ∀ x z y φ
6 nf5 ⊢ Ⅎ x φ ↔ ∀ x φ → ∀ x φ
7 6 sbbii ⊢ z y Ⅎ x φ ↔ z y ∀ x φ → ∀ x φ
8 sbal ⊢ z y ∀ x φ → ∀ x φ ↔ ∀ x z y φ → ∀ x φ
9 7 8 bitri ⊢ z y Ⅎ x φ ↔ ∀ x z y φ → ∀ x φ
10 nf5 ⊢ Ⅎ x z y φ ↔ ∀ x z y φ → ∀ x z y φ
11 5 9 10 3bitr4i ⊢ z y Ⅎ x φ ↔ Ⅎ x z y φ