Theorem eximdv 1933

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
eximdv	|- ( ph -> ( E. x ps -> E. x ch ) )

Distinct variable group:   ph, x

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

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximdh 1664	1 |- ( ph -> ( E. x ps -> E. x ch ) )

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  2eximdv  1935  reximdv2  2649  cgsexg  2857  spc3egv  2917  euind  3013  ssel  3242  reupick  3517  reximdva0m  3537  uniss  3956  eusvnfb  4602  coss1  4937  coss2  4938  ssrelrn  4974  dmss  4982  dmcosseq  5056  funssres  5423  imain  5466  brprcneu  5691  fv3  5721  dffo4  5859  dffo5  5860  f1eqcocnv  6000  mapsnd  6974  mapsn  6976  en2m  7117  ctssdccl  7457  acfun  7569  ccfunen  7636  cc4f  7641  cc4n  7643  dmaddpq  7752  dmmulpq  7753  recexprlemlol  7999  recexprlemupu  8001  ioom  10712  ctinfom  13377  ctinf  13379  omctfn  13392  nninfdclemp1  13399  ptex  13677  subgintm  14060  txcn  15501