Metamath Proof Explorer


Theorem reximddv2

Description: Double deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses reximddv2.1 φ x A y B ψ χ
reximddv2.2 φ x A y B ψ
Assertion reximddv2 φ x A y B χ

Proof

Step Hyp Ref Expression
1 reximddv2.1 φ x A y B ψ χ
2 reximddv2.2 φ x A y B ψ
3 1 ex φ x A y B ψ χ
4 3 reximdva φ x A y B ψ y B χ
5 4 impr φ x A y B ψ y B χ
6 5 2 reximddv φ x A y B χ