Theorem alimdv 1872

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

Syntax hints:   -> wi 4   A.wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-17 1519

This theorem is referenced by:  2alimdv  1874  moim  2083  ralimdv2  2540  sstr2  3154  reuss2  3407  ssuni  3818  disjss2  3969  disjss1  3972  disjiun  3984  exmidsssnc  4189  soss  4299  alxfr  4446  ssrel  4699  ssrel2  4701  ssrelrel  4711  iotaval  5171  omnimkv  7132