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

Metamath Proof Explorer

Theorem eloprabg

Description: The law of concretion for operation class abstraction. Compare elopab . (Contributed by NM, 14-Sep-1999) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses eloprabg.1 ⊢ x = A → φ ↔ ψ
eloprabg.2 ⊢ y = B → ψ ↔ χ
eloprabg.3 ⊢ z = C → χ ↔ θ
Assertion eloprabg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A B C ∈ x y z | φ ↔ θ

Proof

Step Hyp Ref Expression
1 eloprabg.1 ⊢ x = A → φ ↔ ψ
2 eloprabg.2 ⊢ y = B → ψ ↔ χ
3 eloprabg.3 ⊢ z = C → χ ↔ θ
4 1 2 3 syl3an9b ⊢ x = A ∧ y = B ∧ z = C → φ ↔ θ
5 4 eloprabga ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → A B C ∈ x y z | φ ↔ θ