Theorem alimdv 1774

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

Syntax hints:   -> wi 4   A.wal 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1680  ax-4 1693  ax-5 1769

This theorem is referenced by:  2alimdv  1776  ax12v  1945  axc9lem1  2104  axc16i  2167  ralimdv2  2807  mo2icl  3229  sstr2  3451  reuss2  3735  ssuni  4234  disjss2  4392  disjss1  4395  disjiun  4409  disjss3  4417  alxfr  4630  frss  4823  ssrel  4945  ssrel2  4947  ssrelrel  4957  iotaval  5580  fvn0ssdmfun  6041  dff3  6063  dfwe2  6640  ordom  6733  findcard3  7845  dffi2  7968  indcardi  8503  zorn2lem4  8960  uzindi  12232  caubnd  13476  ramtlecl  15006  psgnunilem4  17193  dfcon2  20489  wilthlem3  24051  nbcusgra  25247  disjss1f  28237  ssrelf  28274  ss2mcls  30256  mclsax  30257  wzel  30557  onsuct0  31151  bj-ssbim  31280  wl-ax12v2  31955  axc11next  36802  nrhmzr  40242