Theorem alimdv 1845

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

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem is referenced by:  2alimdv  1847  ax12v2  2049  ax12vOLD  2050  ax12vOLDOLD  2051  ax13lem1  2248  axc16i  2322  ralimdv2  2961  mo2icl  3385  sstr2  3610  reuss2  3907  ssuni  4459  ssuniOLD  4460  disjss2  4623  disjss1  4626  disjiun  4640  disjss3  4652  alxfr  4878  frss  5081  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  iotaval  5862  fvn0ssdmfun  6350  dff3  6372  dfwe2  6981  ordom  7074  findcard3  8203  dffi2  8329  indcardi  8864  zorn2lem4  9321  uzindi  12781  caubnd  14098  ramtlecl  15704  psgnunilem4  17917  dfconn2  21222  wilthlem3  24796  disjss1f  29386  ssrelf  29425  ss2mcls  31465  mclsax  31466  wzel  31771  wzelOLD  31772  onsuct0  32440  bj-ssbim  32621  wl-ax13lem1  33287  wl-ax8clv2  33381  axc11next  38607  nrhmzr  41873  setrec1lem2  42435