# Metamath Proof Explorer

## Theorem rspc3v

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005)

Ref Expression
Hypotheses rspc3v.1 ${⊢}{x}={A}\to \left({\phi }↔{\chi }\right)$
rspc3v.2 ${⊢}{y}={B}\to \left({\chi }↔{\theta }\right)$
rspc3v.3 ${⊢}{z}={C}\to \left({\theta }↔{\psi }\right)$
Assertion rspc3v ${⊢}\left({A}\in {R}\wedge {B}\in {S}\wedge {C}\in {T}\right)\to \left(\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 rspc3v.1 ${⊢}{x}={A}\to \left({\phi }↔{\chi }\right)$
2 rspc3v.2 ${⊢}{y}={B}\to \left({\chi }↔{\theta }\right)$
3 rspc3v.3 ${⊢}{z}={C}\to \left({\theta }↔{\psi }\right)$
4 1 ralbidv ${⊢}{x}={A}\to \left(\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
5 2 ralbidv ${⊢}{y}={B}\to \left(\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\chi }↔\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\theta }\right)$
6 4 5 rspc2v ${⊢}\left({A}\in {R}\wedge {B}\in {S}\right)\to \left(\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\theta }\right)$
7 3 rspcv ${⊢}{C}\in {T}\to \left(\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\theta }\to {\psi }\right)$
8 6 7 sylan9 ${⊢}\left(\left({A}\in {R}\wedge {B}\in {S}\right)\wedge {C}\in {T}\right)\to \left(\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$
9 8 3impa ${⊢}\left({A}\in {R}\wedge {B}\in {S}\wedge {C}\in {T}\right)\to \left(\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\forall {z}\in {T}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$