This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reximd2a

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Hypotheses reximd2a.1 
|- F/ x ph
reximd2a.2 
|- ( ( ( ph /\ x e. A ) /\ ps ) -> x e. B )
reximd2a.3 
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
reximd2a.4 
|- ( ph -> E. x e. A ps )
Assertion reximd2a 
|- ( ph -> E. x e. B ch )

Proof

Step Hyp Ref Expression
1 reximd2a.1 
 |-  F/ x ph
2 reximd2a.2 
 |-  ( ( ( ph /\ x e. A ) /\ ps ) -> x e. B )
3 reximd2a.3 
 |-  ( ( ( ph /\ x e. A ) /\ ps ) -> ch )
4 reximd2a.4 
 |-  ( ph -> E. x e. A ps )
5 2 3 jca 
 |-  ( ( ( ph /\ x e. A ) /\ ps ) -> ( x e. B /\ ch ) )
6 5 expl 
 |-  ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )
7 1 6 eximd 
 |-  ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
8 df-rex 
 |-  ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
9 df-rex 
 |-  ( E. x e. B ch <-> E. x ( x e. B /\ ch ) )
10 7 8 9 3imtr4g 
 |-  ( ph -> ( E. x e. A ps -> E. x e. B ch ) )
11 4 10 mpd 
 |-  ( ph -> E. x e. B ch )