Metamath Proof Explorer


Theorem reximdv2

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by NM, 17-Sep-2003)

Ref Expression
Hypothesis reximdv2.1 φ x A ψ x B χ
Assertion reximdv2 φ x A ψ x B χ

Proof

Step Hyp Ref Expression
1 reximdv2.1 φ x A ψ x B χ
2 1 eximdv φ x x A ψ x x B χ
3 df-rex x A ψ x x A ψ
4 df-rex x B χ x x B χ
5 2 3 4 3imtr4g φ x A ψ x B χ