Theorem eximdv 1929

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

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1931  reximdv2  2643  cgsexg  2851  spc3egv  2911  euind  3007  ssel  3236  reupick  3509  reximdva0m  3528  uniss  3940  eusvnfb  4580  coss1  4915  coss2  4916  ssrelrn  4952  dmss  4960  dmcosseq  5034  funssres  5400  imain  5443  brprcneu  5668  fv3  5698  dffo4  5830  dffo5  5831  f1eqcocnv  5970  mapsnd  6936  mapsn  6938  en2m  7079  ctssdccl  7415  acfun  7527  ccfunen  7594  cc4f  7599  cc4n  7601  dmaddpq  7710  dmmulpq  7711  recexprlemlol  7957  recexprlemupu  7959  ioom  10644  ctinfom  13263  ctinf  13265  omctfn  13278  nninfdclemp1  13285  ptex  13561  subgintm  13951  txcn  15266