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

Metamath Proof Explorer

Theorem vtocl4g

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019)

Ref Expression
Hypotheses vtocl4g.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
vtocl4g.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
vtocl4g.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜌 ) )
vtocl4g.4 ⊢ ( 𝑤 = 𝐷 → ( 𝜌 ↔ 𝜃 ) )
vtocl4g.5 ⊢ 𝜑
Assertion vtocl4g ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 vtocl4g.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 vtocl4g.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3 vtocl4g.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜌 ) )
4 vtocl4g.4 ⊢ ( 𝑤 = 𝐷 → ( 𝜌 ↔ 𝜃 ) )
5 vtocl4g.5 ⊢ 𝜑
6 3 imbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜌 ) ) )
7 4 imbi2d ⊢ ( 𝑤 = 𝐷 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜌 ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) ) )
8 1 2 5 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 )
9 6 7 8 vtocl2g ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) → ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) )
10 9 impcom ⊢ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 )