Metamath Proof Explorer

Theorem ralimd6v

Description: Deduction sextupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 5-Mar-2025)

		Ref	Expression
	Hypothesis	ralim6dv.1	\|- ( ph -> ( ps -> ch ) )
	Assertion	ralimd6v	\|- ( ph -> ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ps -> A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ch ) )

Step	Hyp	Ref	Expression
1		ralim6dv.1	\|- ( ph -> ( ps -> ch ) )
2	1	ralimdvv	\|- ( ph -> ( A. p e. E A. q e. F ps -> A. p e. E A. q e. F ch ) )
3	2	ralimd4v	\|- ( ph -> ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ps -> A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ch ) )

Step

Hyp

Ref

Expression

ralim6dv.1

 |-  ( ph -> ( ps -> ch ) )

 |-  ( ph -> ( A. p e. E A. q e. F ps -> A. p e. E A. q e. F ch ) )

 |-  ( ph -> ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ps -> A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ch ) )