Theorem iotabidv 5241

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

Hypothesis

Ref	Expression
iotabidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
iotabidv	|- ( ph -> ( iota x ps ) = ( iota x ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem iotabidv

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

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1362   = wceq 1364   iotacio 5217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3840  df-iota 5219

This theorem is referenced by:  csbiotag  5251  dffv3g  5554  fveq1  5557  fveq2  5558  fvres  5582  csbfv12g  5596  fvco2  5630  riotaeqdv  5878  riotabidv  5879  riotabidva  5894  ovtposg  6317  shftval  10990  sumeq1  11520  sumeq2  11524  zsumdc  11549  isumclim3  11588  isumshft  11655  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  zproddc  11744  pcval  12465  grpidvalg  13016  grpidpropdg  13017  igsumvalx  13032  gsumpropd  13035  gsumpropd2  13036  gsumress  13038  gsumval2  13040  dfur2g  13518  oppr0g  13637  oppr1g  13638