Theorem alimdv 1757

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1677. (Contributed by NM, 3-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
alimdv	|- ( ph -> ( A. x ps -> A. x ch ) )

Distinct variable group:   ph, x

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

Proof of Theorem alimdv

Step	Hyp	Ref	Expression
1		ax-5 1752	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	alimdh 1683	1 |- ( ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem is referenced by:  2alimdv  1759  ax12v  1910  axc9lem1  2059  axc16i  2123  ralimdv2  2829  mo2icl  3249  sstr2  3471  reuss2  3753  ssuni  4241  disjss2  4397  disjss1  4400  disjiun  4414  disjss3  4422  alxfr  4634  frss  4820  ssrel  4942  ssrel2  4944  ssrelrel  4954  iotaval  5576  fvn0ssdmfun  6028  dff3  6050  dfwe2  6622  ordom  6715  findcard3  7823  dffi2  7946  indcardi  8479  zorn2lem4  8936  uzindi  12200  caubnd  13421  ramtlecl  14950  psgnunilem4  17137  dfcon2  20432  wilthlem3  23993  nbcusgra  25189  disjss1f  28185  ssrelf  28223  ss2mcls  30214  mclsax  30215  wzel  30514  onsuct0  31106  wl-ax12v2  31873  axc11next  36727  nrhmzr  39493