Metamath Proof Explorer

Theorem iscnrm3lem2

Description: Lemma for iscnrm3 proving a biconditional on restricted universal quantifications. (Contributed by Zhi Wang, 3-Sep-2024)

Ref Expression
Hypotheses iscnrm3lem2.1 ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ψ → w ∈ D ∧ v ∈ E → χ
iscnrm3lem2.2 ⊢ φ → ∀ w ∈ D ∀ v ∈ E χ → x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
Assertion iscnrm3lem2 ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ψ ↔ ∀ w ∈ D ∀ v ∈ E χ

Proof

Step Hyp Ref Expression
1 iscnrm3lem2.1 ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ψ → w ∈ D ∧ v ∈ E → χ
2 iscnrm3lem2.2 ⊢ φ → ∀ w ∈ D ∀ v ∈ E χ → x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
3 2ax5 ⊢ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ → ∀ w ∀ v ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
4 r3al ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ψ ↔ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
5 4 1 syl5bir ⊢ φ → ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ → w ∈ D ∧ v ∈ E → χ
6 5 2alimdv ⊢ φ → ∀ w ∀ v ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ → ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
7 3 6 syl5 ⊢ φ → ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ → ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
8 2ax5 ⊢ ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → ∀ y ∀ z ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
9 8 alrimiv ⊢ ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → ∀ x ∀ y ∀ z ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
10 r2al ⊢ ∀ w ∈ D ∀ v ∈ E χ ↔ ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
11 10 2 syl5bir ⊢ φ → ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
12 11 2alimdv ⊢ φ → ∀ y ∀ z ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
13 12 alimdv ⊢ φ → ∀ x ∀ y ∀ z ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
14 9 13 syl5 ⊢ φ → ∀ w ∀ v w ∈ D ∧ v ∈ E → χ → ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ
15 7 14 impbid ⊢ φ → ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → ψ ↔ ∀ w ∀ v w ∈ D ∧ v ∈ E → χ
16 15 4 10 3bitr4g ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ψ ↔ ∀ w ∈ D ∀ v ∈ E χ