Metamath Proof Explorer


Theorem ralimdvv

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

Ref Expression
Hypothesis ralimdvv.1
|- ( ph -> ( ps -> ch ) )
Assertion ralimdvv
|- ( ph -> ( A. x e. A A. y e. B ps -> A. x e. A A. y e. B ch ) )

Proof

Step Hyp Ref Expression
1 ralimdvv.1
 |-  ( ph -> ( ps -> ch ) )
2 1 adantr
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )
3 2 ralimdvva
 |-  ( ph -> ( A. x e. A A. y e. B ps -> A. x e. A A. y e. B ch ) )