Theorem rcla43v 1885

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 1666	. . . 4 |- (x = A -> (A.z e. T ph <-> A.z e. T ch))
3		rcla43v.2	. . . . 5 |- (y = B -> (ch <-> th))
4	3	ralbidv 1666	. . . 4 |- (y = B -> (A.z e. T ch <-> A.z e. T th))
5	2, 4	rcla42v 1883	. . 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 1876	. . 3 |- (C e. T -> (A.z e. T th -> ps))
8	5, 7	sylan9 470	. 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 830	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 777   = wceq 958   e. wcel 960  A.wral 1648

This theorem is referenced by:  mettri2 7810  mettri4 7811  grpass 8044  ringdi 8142  ringdir 8143  ringass 8144  vcdi 8167  vcdir 8168  vcass 8169  lnolin 8411  lnoplt 9833  lnfnlt 9850  cmpasso 10677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815

Copyright terms: Public domain