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 ( ( ( 𝐴𝑄𝐵𝑅 ) ∧ ( 𝐶𝑆𝐷𝑇 ) ) → 𝜃 )