Metamath Proof Explorer

Theorem raltp

Description: Convert a universal quantification over an unordered triple to a conjunction. (Contributed by NM, 13-Sep-2011) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses raltp.1 ⊢ A ∈ V
raltp.2 ⊢ B ∈ V
raltp.3 ⊢ C ∈ V
raltp.4 ⊢ x = A → φ ↔ ψ
raltp.5 ⊢ x = B → φ ↔ χ
raltp.6 ⊢ x = C → φ ↔ θ
Assertion raltp ⊢ ∀ x ∈ A B C φ ↔ ψ ∧ χ ∧ θ

Proof

Step Hyp Ref Expression
1 raltp.1 ⊢ A ∈ V
2 raltp.2 ⊢ B ∈ V
3 raltp.3 ⊢ C ∈ V
4 raltp.4 ⊢ x = A → φ ↔ ψ
5 raltp.5 ⊢ x = B → φ ↔ χ
6 raltp.6 ⊢ x = C → φ ↔ θ
7 4 5 6 raltpg ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ∀ x ∈ A B C φ ↔ ψ ∧ χ ∧ θ
8 1 2 3 7 mp3an ⊢ ∀ x ∈ A B C φ ↔ ψ ∧ χ ∧ θ