Theorem iotabidv 5242

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 5229	. 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 5218

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 3841  df-iota 5220

This theorem is referenced by:  csbiotag  5252  dffv3g  5557  fveq1  5560  fveq2  5561  fvres  5585  csbfv12g  5599  fvco2  5633  riotaeqdv  5881  riotabidv  5882  riotabidva  5897  ovtposg  6326  shftval  11007  sumeq1  11537  sumeq2  11541  zsumdc  11566  isumclim3  11605  isumshft  11672  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  zproddc  11761  pcval  12490  grpidvalg  13075  grpidpropdg  13076  igsumvalx  13091  gsumpropd  13094  gsumpropd2  13095  gsumress  13097  gsumval2  13099  dfur2g  13594  oppr0g  13713  oppr1g  13714