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 φxAyBψχ
reximddv2.2 φxAyBψ
Assertion reximddv2 φxAyBχ

Proof

Step Hyp Ref Expression
1 reximddv2.1 φxAyBψχ
2 reximddv2.2 φxAyBψ
3 1 ex φxAyBψχ
4 3 reximdva φxAyBψyBχ
5 4 impr φxAyBψyBχ
6 5 2 reximddv φxAyBχ