Theorem alimdv 1902

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

Syntax hints:   -> wi 4   A.wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1470  ax-gen 1472  ax-17 1549

This theorem is referenced by:  2alimdv  1904  moim  2118  ralimdv2  2576  sstr2  3200  reuss2  3453  ssuni  3872  disjss2  4024  disjss1  4027  disjiun  4040  exmidsssnc  4248  soss  4362  alxfr  4509  ssrel  4764  ssrel2  4766  ssrelrel  4776  iotaval  5244  omnimkv  7260