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  5972  riotabidv  5973  riotabidva  5989  ovtposg  6425  shftval  11403  sumeq1  11933  sumeq2  11937  zsumdc  11963  isumclim3  12002  isumshft  12069  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  zproddc  12158  pcval  12887  grpidvalg  13474  grpidpropdg  13475  igsumvalx  13490  gsumpropd  13493  gsumpropd2  13494  gsumress  13496  gsumval2  13498  dfur2g  13994  oppr0g  14113  oppr1g  14114  gfsumval  16732