This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexlimdvvva

Description: Inference from Theorem 19.23 of Margaris p. 90, for three restricted quantifiers. (Contributed by AV, 23-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 rexlimdvvva.1 
 |-  ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ( ps -> ch ) )
2 df-3an 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) <-> ( ( x e. A /\ y e. B ) /\ z e. C ) )
3 1 ex 
 |-  ( ph -> ( ( x e. A /\ y e. B /\ z e. C ) -> ( ps -> ch ) ) )
4 2 3 biimtrrid 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z e. C ) -> ( ps -> ch ) ) )
5 4 expdimp 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z e. C -> ( ps -> ch ) ) )
6 5 rexlimdv 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( E. z e. C ps -> ch ) )
7 6 rexlimdvva 
 |-  ( ph -> ( E. x e. A E. y e. B E. z e. C ps -> ch ) )