Metamath Proof Explorer


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 )