Metamath Proof Explorer


Theorem reximdva

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

Ref Expression
Hypothesis reximdva.1 φ x A ψ χ
Assertion reximdva φ x A ψ x A χ

Proof

Step Hyp Ref Expression
1 reximdva.1 φ x A ψ χ
2 1 ex φ x A ψ χ
3 2 reximdvai φ x A ψ x A χ