Metamath Proof Explorer

Theorem wl-sbcom2d

Description: Version of sbcom2 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019)

Ref Expression
Hypotheses wl-sbcom2d.1 ⊢ φ → ¬ ∀ x x = w
wl-sbcom2d.2 ⊢ φ → ¬ ∀ x x = z
wl-sbcom2d.3 ⊢ φ → ¬ ∀ z z = y
Assertion wl-sbcom2d ⊢ φ → w z y x ψ ↔ y x w z ψ

Proof

Step Hyp Ref Expression
1 wl-sbcom2d.1 ⊢ φ → ¬ ∀ x x = w
2 wl-sbcom2d.2 ⊢ φ → ¬ ∀ x x = z
3 wl-sbcom2d.3 ⊢ φ → ¬ ∀ z z = y
4 ax6ev ⊢ ∃ u u = y
5 ax6ev ⊢ ∃ v v = w
6 wl-sbcom2d-lem2 ⊢ ¬ ∀ z z = x → u x v z ψ ↔ ∀ x ∀ z x = u ∧ z = v → ψ
7 alcom ⊢ ∀ x ∀ z x = u ∧ z = v → ψ ↔ ∀ z ∀ x x = u ∧ z = v → ψ
8 ancomst ⊢ x = u ∧ z = v → ψ ↔ z = v ∧ x = u → ψ
9 8 2albii ⊢ ∀ z ∀ x x = u ∧ z = v → ψ ↔ ∀ z ∀ x z = v ∧ x = u → ψ
10 7 9 bitri ⊢ ∀ x ∀ z x = u ∧ z = v → ψ ↔ ∀ z ∀ x z = v ∧ x = u → ψ
11 6 10 bitrdi ⊢ ¬ ∀ z z = x → u x v z ψ ↔ ∀ z ∀ x z = v ∧ x = u → ψ
12 11 naecoms ⊢ ¬ ∀ x x = z → u x v z ψ ↔ ∀ z ∀ x z = v ∧ x = u → ψ
13 wl-sbcom2d-lem2 ⊢ ¬ ∀ x x = z → v z u x ψ ↔ ∀ z ∀ x z = v ∧ x = u → ψ
14 12 13 bitr4d ⊢ ¬ ∀ x x = z → u x v z ψ ↔ v z u x ψ
15 2 14 syl ⊢ φ → u x v z ψ ↔ v z u x ψ
16 15 adantl ⊢ u = y ∧ v = w ∧ φ → u x v z ψ ↔ v z u x ψ
17 wl-sbcom2d-lem1 ⊢ u = y ∧ v = w → ¬ ∀ x x = w → u x v z ψ ↔ y x w z ψ
18 1 17 syl5 ⊢ u = y ∧ v = w → φ → u x v z ψ ↔ y x w z ψ
19 18 imp ⊢ u = y ∧ v = w ∧ φ → u x v z ψ ↔ y x w z ψ
20 wl-sbcom2d-lem1 ⊢ v = w ∧ u = y → ¬ ∀ z z = y → v z u x ψ ↔ w z y x ψ
21 3 20 syl5 ⊢ v = w ∧ u = y → φ → v z u x ψ ↔ w z y x ψ
22 21 ancoms ⊢ u = y ∧ v = w → φ → v z u x ψ ↔ w z y x ψ
23 22 imp ⊢ u = y ∧ v = w ∧ φ → v z u x ψ ↔ w z y x ψ
24 16 19 23 3bitr3rd ⊢ u = y ∧ v = w ∧ φ → w z y x ψ ↔ y x w z ψ
25 24 exp31 ⊢ u = y → v = w → φ → w z y x ψ ↔ y x w z ψ
26 25 exlimdv ⊢ u = y → ∃ v v = w → φ → w z y x ψ ↔ y x w z ψ
27 26 exlimiv ⊢ ∃ u u = y → ∃ v v = w → φ → w z y x ψ ↔ y x w z ψ
28 4 5 27 mp2 ⊢ φ → w z y x ψ ↔ y x w z ψ