Theorem alimdv 1851

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

Syntax hints:   -> wi 4   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-17 1506

This theorem is referenced by:  2alimdv  1853  moim  2061  ralimdv2  2500  sstr2  3099  reuss2  3351  ssuni  3753  disjss2  3904  disjss1  3907  disjiun  3919  exmidsssnc  4121  soss  4231  alxfr  4377  ssrel  4622  ssrel2  4624  ssrelrel  4634  iotaval  5094  omnimkv  7023