Metamath Proof Explorer


Theorem rspc3dv

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses rspc3dv.1 ( 𝑥 = 𝐴 → ( 𝜓𝜃 ) )
rspc3dv.2 ( 𝑦 = 𝐵 → ( 𝜃𝜏 ) )
rspc3dv.3 ( 𝑧 = 𝐶 → ( 𝜏𝜒 ) )
rspc3dv.4 ( 𝜑 → ∀ 𝑥𝐷𝑦𝐸𝑧𝐹 𝜓 )
rspc3dv.5 ( 𝜑𝐴𝐷 )
rspc3dv.6 ( 𝜑𝐵𝐸 )
rspc3dv.7 ( 𝜑𝐶𝐹 )
Assertion rspc3dv ( 𝜑𝜒 )

Proof

Step Hyp Ref Expression
1 rspc3dv.1 ( 𝑥 = 𝐴 → ( 𝜓𝜃 ) )
2 rspc3dv.2 ( 𝑦 = 𝐵 → ( 𝜃𝜏 ) )
3 rspc3dv.3 ( 𝑧 = 𝐶 → ( 𝜏𝜒 ) )
4 rspc3dv.4 ( 𝜑 → ∀ 𝑥𝐷𝑦𝐸𝑧𝐹 𝜓 )
5 rspc3dv.5 ( 𝜑𝐴𝐷 )
6 rspc3dv.6 ( 𝜑𝐵𝐸 )
7 rspc3dv.7 ( 𝜑𝐶𝐹 )
8 5 6 7 3jca ( 𝜑 → ( 𝐴𝐷𝐵𝐸𝐶𝐹 ) )
9 1 2 3 rspc3v ( ( 𝐴𝐷𝐵𝐸𝐶𝐹 ) → ( ∀ 𝑥𝐷𝑦𝐸𝑧𝐹 𝜓𝜒 ) )
10 8 4 9 sylc ( 𝜑𝜒 )