Theorem eximdv 1868

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 1514	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximdh 1599	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1870  reximdv2  2564  cgsexg  2760  spc3egv  2817  euind  2912  ssel  3135  reupick  3405  reximdva0m  3423  uniss  3809  eusvnfb  4431  coss1  4758  coss2  4759  dmss  4802  dmcosseq  4874  funssres  5229  imain  5269  brprcneu  5478  fv3  5508  dffo4  5632  dffo5  5633  f1eqcocnv  5758  mapsn  6652  ctssdccl  7072  acfun  7159  ccfunen  7201  cc4f  7206  cc4n  7208  dmaddpq  7316  dmmulpq  7317  recexprlemlol  7563  recexprlemupu  7565  ioom  10192  ctinfom  12357  ctinf  12359  omctfn  12372  nninfdclemp1  12379  txcn  12875