Metamath Proof Explorer


Theorem ralimda

Description: Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses ralimda.1
|- F/ x ph
ralimda.2
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
Assertion ralimda
|- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Proof

Step Hyp Ref Expression
1 ralimda.1
 |-  F/ x ph
2 ralimda.2
 |-  ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3 nfra1
 |-  F/ x A. x e. A ps
4 1 3 nfan
 |-  F/ x ( ph /\ A. x e. A ps )
5 id
 |-  ( ( ph /\ x e. A ) -> ( ph /\ x e. A ) )
6 5 adantlr
 |-  ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ( ph /\ x e. A ) )
7 rspa
 |-  ( ( A. x e. A ps /\ x e. A ) -> ps )
8 7 adantll
 |-  ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ps )
9 6 8 2 sylc
 |-  ( ( ( ph /\ A. x e. A ps ) /\ x e. A ) -> ch )
10 4 9 ralrimia
 |-  ( ( ph /\ A. x e. A ps ) -> A. x e. A ch )
11 10 ex
 |-  ( ph -> ( A. x e. A ps -> A. x e. A ch ) )