This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r3al

Description: Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995) (Proof shortened by Wolf Lammen, 30-Dec-2019)

Ref Expression
Assertion r3al ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → φ

Proof

Step Hyp Ref Expression
1 r2al ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ∀ z ∈ C φ
2 19.21v ⊢ ∀ z x ∈ A ∧ y ∈ B → z ∈ C → φ ↔ x ∈ A ∧ y ∈ B → ∀ z z ∈ C → φ
3 df-3an ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C
4 3 imbi1i ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C → φ ↔ x ∈ A ∧ y ∈ B ∧ z ∈ C → φ
5 impexp ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C → φ ↔ x ∈ A ∧ y ∈ B → z ∈ C → φ
6 4 5 bitri ⊢ x ∈ A ∧ y ∈ B ∧ z ∈ C → φ ↔ x ∈ A ∧ y ∈ B → z ∈ C → φ
7 6 albii ⊢ ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → φ ↔ ∀ z x ∈ A ∧ y ∈ B → z ∈ C → φ
8 df-ral ⊢ ∀ z ∈ C φ ↔ ∀ z z ∈ C → φ
9 8 imbi2i ⊢ x ∈ A ∧ y ∈ B → ∀ z ∈ C φ ↔ x ∈ A ∧ y ∈ B → ∀ z z ∈ C → φ
10 2 7 9 3bitr4ri ⊢ x ∈ A ∧ y ∈ B → ∀ z ∈ C φ ↔ ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → φ
11 10 2albii ⊢ ∀ x ∀ y x ∈ A ∧ y ∈ B → ∀ z ∈ C φ ↔ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → φ
12 1 11 bitri ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C φ ↔ ∀ x ∀ y ∀ z x ∈ A ∧ y ∈ B ∧ z ∈ C → φ