Theorem alimdv 1685

Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (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 1680	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	alimdh 1618	1 |- ( ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1377

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

This theorem is referenced by:  2alimdv  1687  ax12v  1804  axc9lem1  1970  axc16i  2037  morimvOLD  2344  ralimdv2  2871  mo2icl  3282  sstr2  3511  reuss2  3778  ssuni  4267  disjss2  4420  disjss1  4423  disjiun  4437  disjss3  4446  alxfr  4660  frss  4846  ssrel  5089  ssrel2  5091  ssrelrel  5101  iotaval  5560  dff3  6032  dfwe2  6595  ordom  6687  findcard3  7759  dffi2  7879  indcardi  8418  zorn2lem4  8875  uzindi  12055  caubnd  13150  ramtlecl  14373  psgnunilem4  16318  bwthOLD  19677  dfcon2  19686  wilthlem3  23072  nbcusgra  24139  disjss1f  27108  wzel  28957  onsuct0  29483  axc11next  30891