Theorem exbid

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

	Ref	Expression
Hypotheses	albid.1	|- F/ x ph
	albid.2	|- ( ph -> ( ps <-> ch ) )
Assertion	exbid	|- ( ph -> ( E. x ps <-> E. 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	exbidh	|- ( ph -> ( E. x ps <-> E. x ch ) )