Metamath Proof Explorer


Theorem ralimda

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

Ref Expression
Hypotheses ralimda.1 x φ
ralimda.2 φ x A ψ χ
Assertion ralimda φ x A ψ x A χ

Proof

Step Hyp Ref Expression
1 ralimda.1 x φ
2 ralimda.2 φ x A ψ χ
3 nfra1 x x A ψ
4 1 3 nfan x φ x A ψ
5 id φ x A φ x A
6 5 adantlr φ x A ψ x A φ x A
7 rspa x A ψ x A ψ
8 7 adantll φ x A ψ x A ψ
9 6 8 2 sylc φ x A ψ x A χ
10 4 9 ralrimia φ x A ψ x A χ
11 10 ex φ x A ψ x A χ