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  4600  coss1  4935  coss2  4936  ssrelrn  4972  dmss  4980  dmcosseq  5054  funssres  5420  imain  5463  brprcneu  5688  fv3  5718  dffo4  5856  dffo5  5857  f1eqcocnv  5997  mapsnd  6970  mapsn  6972  en2m  7113  ctssdccl  7452  acfun  7564  ccfunen  7631  cc4f  7636  cc4n  7638  dmaddpq  7747  dmmulpq  7748  recexprlemlol  7994  recexprlemupu  7996  ioom  10706  ctinfom  13370  ctinf  13372  omctfn  13385  nninfdclemp1  13392  ptex  13669  subgintm  14052  txcn  15428