Theorem alimdv 1676

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 1671	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	alimdh 1609	1 |- ( ph -> ( A. x ps -> A. x ch ) )

Syntax hints:   -> wi 4   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1592  ax-4 1603  ax-5 1671

This theorem is referenced by:  2alimdv  1678  axc9lem1  1954  axc16i  2021  morimvOLD  2329  ralimdv2  2898  mo2icl  3238  sstr2  3464  reuss2  3731  ssuni  4214  disjss2  4366  disjss1  4369  disjiun  4383  disjss3  4392  alxfr  4606  frss  4788  ssrel  5029  ssrel2  5031  ssrelrel  5041  iotaval  5493  dff3  5958  dfwe2  6496  ordom  6588  findcard3  7659  dffi2  7777  indcardi  8315  zorn2lem4  8772  uzindi  11913  caubnd  12957  ramtlecl  14172  psgnunilem4  16114  bwthOLD  19139  dfcon2  19148  wilthlem3  22534  nbcusgra  23516  disjss1f  26062  wzel  27898  onsuct0  28424  axc11next  29801