Theorem albid

Description: Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016)

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

Proof

Step	Hyp	Ref	Expression
1		albid.1	|- F/ x ph
2		albid.2	|- ( ph -> ( ps <-> ch ) )
3	1	nf5ri	|- ( ph -> A. x ph )
4	3 2	albidh	|- ( ph -> ( A. x ps <-> A. x ch ) )