Theorem eximdv 1622

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.xps -> E.xch))

Distinct variable group:   ph,x

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

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1616	. 2 |- (ph -> A.xph)
2		alimdv.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	eximdh 1588	1 |- (ph -> (E.xps -> E.xch))

Syntax hints:   -> wi 4  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2eximdv  1624  exlimdv  1636  ax12olem2  1928  moim  2250  morimv  2252  reximdv2  2724  cgsexg  2891  spc3egv  2944  euind  3024  ssel  3268  reupick  3540  reximdva0  3562  uniss  3913  nnpw1ex  4485  coss1  4873  coss2  4874  dmss  4907  dmcosseq  4974  funssres  5145  fv3  5342  dffo4  5424  dffo5  5425  fvclss  5463  mapsn  6027  ncspw1eu  6160  taddc  6230  fnfreclem3  6320