Theorem iotabidv 5335

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 1923	. 2 |- ( ph -> A. x ( ps <-> ch ) )
3		iotabi 5322	. 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 1396   = wceq 1398   iotacio 5310

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-uni 3915  df-iota 5312

This theorem is referenced by:  csbiotag  5345  dffv3g  5666  fveq1  5669  fveq2  5670  fvres  5694  csbfv12g  5710  fvco2  5746  riotaeqdv  6004  riotabidv  6005  riotabidva  6021  ovtposg  6490  shftval  11510  sumeq1  12040  sumeq2  12044  zsumdc  12070  isumclim3  12109  isumshft  12176  prodeq1f  12238  prodeq2w  12242  prodeq2  12243  zproddc  12265  pcval  12994  grpidvalg  13586  grpidpropdg  13587  igsumvalx  13602  gsumpropd  13605  gsumpropd2  13606  gsumress  13608  gsumval2  13610  dfur2g  14106  oppr0g  14225  oppr1g  14226  gfsumval  16862