Theorem alimdv 1724

Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1647. (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 1719	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	alimdh 1653	1 |- ( ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1633  ax-4 1646  ax-5 1719

This theorem is referenced by:  2alimdv  1726  ax12v  1873  axc9lem1  2018  axc16i  2080  ralimdv2  2799  mo2icl  3216  sstr2  3437  reuss2  3716  ssuni  4198  disjss2  4354  disjss1  4357  disjiun  4371  disjss3  4379  alxfr  4588  frss  4773  ssrel  5017  ssrel2  5019  ssrelrel  5029  iotaval  5484  fvn0ssdmfun  5937  dff3  5959  dfwe2  6534  ordom  6626  findcard3  7696  dffi2  7816  indcardi  8353  zorn2lem4  8810  uzindi  12013  caubnd  13212  ramtlecl  14539  psgnunilem4  16658  dfcon2  20024  wilthlem3  23480  nbcusgra  24605  disjss1f  27592  ssrelf  27630  ss2mcls  29153  mclsax  29154  wzel  29581  onsuct0  30095  axc11next  31517  nrhmzr  32914