Theorem iotabii

Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		iotabii.1	|- ( ph <-> ps )
2		iotabi	|- ( A. x ( ph <-> ps ) -> ( iota x ph ) = ( iota x ps ) )
3	2 1	mpg	|- ( iota x ph ) = ( iota x ps )