Theorem alimdv 1696

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

Syntax hints:   -> wi 4   A.wal 1381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem is referenced by:  2alimdv  1698  ax12v  1841  axc9lem1  1987  axc16i  2050  morimvOLD  2328  ralimdv2  2850  mo2icl  3264  sstr2  3496  reuss2  3763  ssuni  4256  disjss2  4410  disjss1  4413  disjiun  4427  disjss3  4436  alxfr  4650  frss  4836  ssrel  5081  ssrel2  5083  ssrelrel  5093  iotaval  5552  fvn0ssdmfun  6007  dff3  6029  dfwe2  6602  ordom  6694  findcard3  7765  dffi2  7885  indcardi  8425  zorn2lem4  8882  uzindi  12073  caubnd  13173  ramtlecl  14500  psgnunilem4  16501  bwthOLD  19889  dfcon2  19898  wilthlem3  23322  nbcusgra  24441  disjss1f  27413  ssrelf  27444  ss2mcls  28906  mclsax  28907  wzel  29356  onsuct0  29882  axc11next  31267