Theorem reximddv 3018

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)

Hypotheses

Ref	Expression
reximddva.1	|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
reximddva.2	|- ( ph -> E. x e. A ps )

Assertion

Ref	Expression
reximddv	|- ( ph -> E. x e. A ch )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximddv

Step	Hyp	Ref	Expression
1		reximddva.2	. 2 |- ( ph -> E. x e. A ps )
2		reximddva.1	. . . 4 |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )
3	2	expr 643	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
4	3	reximdva 3017	. 2 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
5	1, 4	mpd 15	1 |- ( ph -> E. x e. A ch )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  reximddv2  3020  dedekind  10200  caucvgrlem  14403  isprm5  15419  drsdirfi  16938  sylow2  18041  gexex  18256  nrmsep  21161  regsep2  21180  locfincmp  21329  dissnref  21331  met1stc  22326  xrge0tsms  22637  cnheibor  22754  lmcau  23111  ismbf3d  23421  ulmdvlem3  24156  legov  25480  legtrid  25486  midexlem  25587  opphllem  25627  mideulem  25628  midex  25629  oppperpex  25645  hpgid  25658  lnperpex  25695  trgcopy  25696  grpoidinv  27362  pjhthlem2  28251  mdsymlem3  29264  xrge0tsmsd  29785  ballotlemfc0  30554  ballotlemfcc  30555  cvmliftlem15  31280  unblimceq0  32498  knoppndvlem18  32520  lhpexle3lem  35297  lhpex2leN  35299  cdlemg1cex  35876  nacsfix  37275  unxpwdom3  37665  rfcnnnub  39195  reximddv3  39343  climxrrelem  39981  climxrre  39982  xlimxrre  40057  stoweidlem27  40244