Theorem albidh

Description: Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993)

	Ref	Expression
Hypotheses	albidh.1	|- ( ph -> A. x ph )
	albidh.2	|- ( ph -> ( ps <-> ch ) )
Assertion	albidh	|- ( ph -> ( A. x ps <-> A. x ch ) )

Proof

Step	Hyp	Ref	Expression
1		albidh.1	|- ( ph -> A. x ph )
2		albidh.2	|- ( ph -> ( ps <-> ch ) )
3	1 2	alrimih	|- ( ph -> A. x ( ps <-> ch ) )
4		albi	|- ( A. x ( ps <-> ch ) -> ( A. x ps <-> A. x ch ) )
5	3 4	syl	|- ( ph -> ( A. x ps <-> A. x ch ) )