Theorem alimdv 1890

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

Syntax hints:   -> wi 4   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460  ax-17 1537

This theorem is referenced by:  2alimdv  1892  moim  2106  ralimdv2  2564  sstr2  3187  reuss2  3440  ssuni  3858  disjss2  4010  disjss1  4013  disjiun  4025  exmidsssnc  4233  soss  4346  alxfr  4493  ssrel  4748  ssrel2  4750  ssrelrel  4760  iotaval  5227  omnimkv  7217