Theorem iotabidv 5309

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 1922	. 2 |- ( ph -> A. x ( ps <-> ch ) )
3		iotabi 5296	. 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 1395   = wceq 1397   iotacio 5284

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-uni 3894  df-iota 5286

This theorem is referenced by:  csbiotag  5319  dffv3g  5635  fveq1  5638  fveq2  5639  fvres  5663  csbfv12g  5679  fvco2  5715  riotaeqdv  5971  riotabidv  5972  riotabidva  5988  ovtposg  6424  shftval  11385  sumeq1  11915  sumeq2  11919  zsumdc  11944  isumclim3  11983  isumshft  12050  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  zproddc  12139  pcval  12868  grpidvalg  13455  grpidpropdg  13456  igsumvalx  13471  gsumpropd  13474  gsumpropd2  13475  gsumress  13477  gsumval2  13479  dfur2g  13974  oppr0g  14093  oppr1g  14094  gfsumval  16680