Theorem alimdv 1867

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

Syntax hints:   -> wi 4   A.wal 1341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1435  ax-gen 1437  ax-17 1514

This theorem is referenced by:  2alimdv  1869  moim  2078  ralimdv2  2536  sstr2  3149  reuss2  3402  ssuni  3811  disjss2  3962  disjss1  3965  disjiun  3977  exmidsssnc  4182  soss  4292  alxfr  4439  ssrel  4692  ssrel2  4694  ssrelrel  4704  iotaval  5164  omnimkv  7120