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

Metamath Proof Explorer

Theorem vtocl4gaOLD

Description: Obsolete version of vtocl4ga as of 31-May-2025. (Contributed by AV, 22-Jan-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 vtocl4ga.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2 vtocl4ga.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3 vtocl4ga.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜌 ) )
4 vtocl4ga.4 ⊢ ( 𝑤 = 𝐷 → ( 𝜌 ↔ 𝜃 ) )
5 vtocl4ga.5 ⊢ ( ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜑 )
6 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑄 ↔ 𝐴 ∈ 𝑄 ) )
7 6 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ↔ ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ) )
8 7 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ) )
9 8 1 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜑 ) ↔ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜓 ) ) )
10 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑅 ↔ 𝐵 ∈ 𝑅 ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ↔ ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ) )
12 11 anbi1d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ) )
13 12 2 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( ( 𝐴 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜓 ) ↔ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜒 ) ) )
14 eleq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ 𝑆 ↔ 𝐶 ∈ 𝑆 ) )
15 14 anbi1d ⊢ ( 𝑧 = 𝐶 → ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ↔ ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) )
16 15 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ) )
17 16 3 imbi12d ⊢ ( 𝑧 = 𝐶 → ( ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜒 ) ↔ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜌 ) ) )
18 eleq1 ⊢ ( 𝑤 = 𝐷 → ( 𝑤 ∈ 𝑇 ↔ 𝐷 ∈ 𝑇 ) )
19 18 anbi2d ⊢ ( 𝑤 = 𝐷 → ( ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ↔ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) )
20 19 anbi2d ⊢ ( 𝑤 = 𝐷 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) ) )
21 20 4 imbi12d ⊢ ( 𝑤 = 𝐷 → ( ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜌 ) ↔ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 ) ) )
22 9 13 17 21 5 vtocl4g ⊢ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 ) )
23 22 pm2.43i ⊢ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 )