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  2723  cgsexg  2890  spc3egv  2943  euind  3023  ssel  3267  reupick  3539  reximdva0  3561  uniss  3912  nnpw1ex  4484  coss1  4872  coss2  4873  dmss  4906  dmcosseq  4973  funssres  5144  fv3  5341  dffo4  5423  dffo5  5424  fvclss  5462  mapsn  6026  ncspw1eu  6159  taddc  6229  fnfreclem3  6319