Metamath Proof Explorer


Theorem vtocl3gaf

Description: Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 31-May-2025)

Ref Expression
Hypotheses vtocl3gaf.a 𝑥 𝐴
vtocl3gaf.b 𝑦 𝐴
vtocl3gaf.c 𝑧 𝐴
vtocl3gaf.d 𝑦 𝐵
vtocl3gaf.e 𝑧 𝐵
vtocl3gaf.f 𝑧 𝐶
vtocl3gaf.1 𝑥 𝜓
vtocl3gaf.2 𝑦 𝜒
vtocl3gaf.3 𝑧 𝜃
vtocl3gaf.4 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
vtocl3gaf.5 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
vtocl3gaf.6 ( 𝑧 = 𝐶 → ( 𝜒𝜃 ) )
vtocl3gaf.7 ( ( 𝑥𝑅𝑦𝑆𝑧𝑇 ) → 𝜑 )
Assertion vtocl3gaf ( ( 𝐴𝑅𝐵𝑆𝐶𝑇 ) → 𝜃 )

Proof

Step Hyp Ref Expression
1 vtocl3gaf.a 𝑥 𝐴
2 vtocl3gaf.b 𝑦 𝐴
3 vtocl3gaf.c 𝑧 𝐴
4 vtocl3gaf.d 𝑦 𝐵
5 vtocl3gaf.e 𝑧 𝐵
6 vtocl3gaf.f 𝑧 𝐶
7 vtocl3gaf.1 𝑥 𝜓
8 vtocl3gaf.2 𝑦 𝜒
9 vtocl3gaf.3 𝑧 𝜃
10 vtocl3gaf.4 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
11 vtocl3gaf.5 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) )
12 vtocl3gaf.6 ( 𝑧 = 𝐶 → ( 𝜒𝜃 ) )
13 vtocl3gaf.7 ( ( 𝑥𝑅𝑦𝑆𝑧𝑇 ) → 𝜑 )
14 3 nfel1 𝑧 𝐴𝑅
15 5 nfel1 𝑧 𝐵𝑆
16 14 15 nfan 𝑧 ( 𝐴𝑅𝐵𝑆 )
17 16 9 nfim 𝑧 ( ( 𝐴𝑅𝐵𝑆 ) → 𝜃 )
18 12 imbi2d ( 𝑧 = 𝐶 → ( ( ( 𝐴𝑅𝐵𝑆 ) → 𝜒 ) ↔ ( ( 𝐴𝑅𝐵𝑆 ) → 𝜃 ) ) )
19 nfv 𝑥 𝑧𝑇
20 19 7 nfim 𝑥 ( 𝑧𝑇𝜓 )
21 nfv 𝑦 𝑧𝑇
22 21 8 nfim 𝑦 ( 𝑧𝑇𝜒 )
23 10 imbi2d ( 𝑥 = 𝐴 → ( ( 𝑧𝑇𝜑 ) ↔ ( 𝑧𝑇𝜓 ) ) )
24 11 imbi2d ( 𝑦 = 𝐵 → ( ( 𝑧𝑇𝜓 ) ↔ ( 𝑧𝑇𝜒 ) ) )
25 13 3expia ( ( 𝑥𝑅𝑦𝑆 ) → ( 𝑧𝑇𝜑 ) )
26 1 2 4 20 22 23 24 25 vtocl2gaf ( ( 𝐴𝑅𝐵𝑆 ) → ( 𝑧𝑇𝜒 ) )
27 26 com12 ( 𝑧𝑇 → ( ( 𝐴𝑅𝐵𝑆 ) → 𝜒 ) )
28 6 17 18 27 vtoclgaf ( 𝐶𝑇 → ( ( 𝐴𝑅𝐵𝑆 ) → 𝜃 ) )
29 28 impcom ( ( ( 𝐴𝑅𝐵𝑆 ) ∧ 𝐶𝑇 ) → 𝜃 )
30 29 3impa ( ( 𝐴𝑅𝐵𝑆𝐶𝑇 ) → 𝜃 )