Theorem eximdv 1853

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

Syntax hints:   -> wi 4   E.wex 1469

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximdv  1855  reximdv2  2534  cgsexg  2724  spc3egv  2781  euind  2875  ssel  3096  reupick  3365  reximdva0m  3383  uniss  3765  eusvnfb  4383  coss1  4702  coss2  4703  dmss  4746  dmcosseq  4818  funssres  5173  imain  5213  brprcneu  5422  fv3  5452  dffo4  5576  dffo5  5577  f1eqcocnv  5700  mapsn  6592  ctssdccl  7004  acfun  7080  ccfunen  7096  cc4f  7101  cc4n  7103  dmaddpq  7211  dmmulpq  7212  recexprlemlol  7458  recexprlemupu  7460  ioom  10069  ctinfom  11977  ctinf  11979  omctfn  11992  txcn  12483