Theorem rcla43v 1882

Description: 3-variable restricted specialization with implicit substitution.

Hypotheses

Ref	Expression
rcla43v.1	|- (x = A -> (ph <-> ch))
rcla43v.2	|- (y = B -> (ch <-> th))
rcla43v.3	|- (z = C -> (th <-> ps))

Assertion

Ref	Expression
rcla43v	|- ((A e. R /\ B e. S /\ C e. T) -> (A.x e. R A.y e. S A.z e. T ph -> ps))

Distinct variable groups:   ps,z   ch,x   th,y   x,y,z,A   y,B,z   z,C   x,R   x,S,y   x,T,y,z

Proof of Theorem rcla43v

Step	Hyp	Ref	Expression
1		rcla43v.1	. . . . 5 |- (x = A -> (ph <-> ch))
2	1	ralbidv 1663	. . . 4 |- (x = A -> (A.z e. T ph <-> A.z e. T ch))
3		rcla43v.2	. . . . 5 |- (y = B -> (ch <-> th))
4	3	ralbidv 1663	. . . 4 |- (y = B -> (A.z e. T ch <-> A.z e. T th))
5	2, 4	rcla42v 1880	. . 3 |- ((A e. R /\ B e. S) -> (A.x e. R A.y e. S A.z e. T ph -> A.z e. T th))
6		rcla43v.3	. . . 4 |- (z = C -> (th <-> ps))
7	6	rcla4v 1873	. . 3 |- (C e. T -> (A.z e. T th -> ps))
8	5, 7	sylan9 468	. 2 |- (((A e. R /\ B e. S) /\ C e. T) -> (A.x e. R A.y e. S A.z e. T ph -> ps))
9	8	3impa 828	1 |- ((A e. R /\ B e. S /\ C e. T) -> (A.x e. R A.y e. S A.z e. T ph -> ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 775   = wceq 956   e. wcel 958  A.wral 1645

This theorem is referenced by:  mettri2 7813  mettri4 7814  grpass 8047  ringdi 8146  ringdir 8147  ringass 8148  vcdi 8171  vcdir 8172  vcass 8173  lnolin 8415  lnoplt 9838  lnfnlt 9855  cmpasso 10706

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812

Copyright terms: Public domain