Metamath Proof Explorer


Theorem ralimdaa

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of Margaris p. 90. (Contributed by NM, 22-Sep-2003) (Proof shortened by Wolf Lammen, 29-Dec-2019)

Ref Expression
Hypotheses ralimdaa.1 xφ
ralimdaa.2 φxAψχ
Assertion ralimdaa φxAψxAχ

Proof

Step Hyp Ref Expression
1 ralimdaa.1 xφ
2 ralimdaa.2 φxAψχ
3 2 ex φxAψχ
4 1 3 ralrimi φxAψχ
5 ralim xAψχxAψxAχ
6 4 5 syl φxAψxAχ