Metamath Proof Explorer

Theorem reximdv

Description: Deduction from Theorem 19.22 of Margaris p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998)

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


Step Hyp Ref Expression
1 reximdv.1 φ ψ χ
2 1 a1d φ x A ψ χ
3 2 reximdvai φ x A ψ x A χ