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  2063  ralimdv2  2502  sstr2  3104  reuss2  3356  ssuni  3758  disjss2  3909  disjss1  3912  disjiun  3924  exmidsssnc  4126  soss  4236  alxfr  4382  ssrel  4627  ssrel2  4629  ssrelrel  4639  iotaval  5099  omnimkv  7030