Theorem alimdv 1852

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

Syntax hints:   -> wi 4   A.wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1424  ax-gen 1426  ax-17 1507

This theorem is referenced by:  2alimdv  1854  moim  2064  ralimdv2  2505  sstr2  3109  reuss2  3361  ssuni  3766  disjss2  3917  disjss1  3920  disjiun  3932  exmidsssnc  4134  soss  4244  alxfr  4390  ssrel  4635  ssrel2  4637  ssrelrel  4647  iotaval  5107  omnimkv  7038