Theorem alimdv 1932

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

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  2alimdv  1934  moim  2151  ralimdv2  2620  sstr2  3255  reuss2  3513  ssuni  3957  disjss2  4109  disjss1  4112  disjiun  4125  exmidsssnc  4340  soss  4459  alxfr  4607  ssrel  4863  ssrel2  4865  ssrelrel  4875  iotaval  5349  omnimkv  7496