Theorem iotabidv

Description: Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011)

	Ref	Expression
Hypothesis	iotabidv.1	|- ( ph -> ( ps <-> ch ) )
Assertion	iotabidv	|- ( ph -> ( iota x ps ) = ( iota x ch ) )

Proof

Step	Hyp	Ref	Expression
1		iotabidv.1	|- ( ph -> ( ps <-> ch ) )
2	1	alrimiv	|- ( ph -> A. x ( ps <-> ch ) )
3		iotabi	|- ( A. x ( ps <-> ch ) -> ( iota x ps ) = ( iota x ch ) )
4	2 3	syl	|- ( ph -> ( iota x ps ) = ( iota x ch ) )