Metamath Proof Explorer


Theorem r19.40

Description: Restricted quantifier version of Theorem 19.40 of Margaris p. 90. (Contributed by NM, 2-Apr-2004)

Ref Expression
Assertion r19.40 xAφψxAφxAψ

Proof

Step Hyp Ref Expression
1 simpl φψφ
2 1 reximi xAφψxAφ
3 simpr φψψ
4 3 reximi xAφψxAψ
5 2 4 jca xAφψxAφxAψ