Metamath Proof Explorer


Theorem rspec3

Description: Specialization rule for restricted quantification, with three quantifiers. (Contributed by NM, 20-Nov-1994)

Ref Expression
Hypothesis rspec3.1
|- A. x e. A A. y e. B A. z e. C ph
Assertion rspec3
|- ( ( x e. A /\ y e. B /\ z e. C ) -> ph )

Proof

Step Hyp Ref Expression
1 rspec3.1
 |-  A. x e. A A. y e. B A. z e. C ph
2 1 rspec2
 |-  ( ( x e. A /\ y e. B ) -> A. z e. C ph )
3 2 r19.21bi
 |-  ( ( ( x e. A /\ y e. B ) /\ z e. C ) -> ph )
4 3 3impa
 |-  ( ( x e. A /\ y e. B /\ z e. C ) -> ph )