Theorem iotabidv 5577

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

Hypothesis

Ref	Expression
iotabidv.1

Assertion

Ref	Expression
iotabidv

Distinct variable group:   ,

Proof of Theorem iotabidv

Step	Hyp	Ref	Expression
1		iotabidv.1	. . 3
2	1	alrimiv 1719	. 2
3		iotabi 5565	. 2
4	2, 3	syl 16	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  iotacio 5554

This theorem is referenced by:  csbiota  5585  csbiotagOLD  5586  dffv3  5867  fveq1  5870  fveq2  5871  fvres  5885  csbfv12  5906  csbfv12gOLD  5907  opabiota  5936  fvco2  5948  fvopab5  5979  riotaeqdv  6258  riotabidv  6259  riotabidva  6274  erov  7427  iunfictbso  8516  isf32lem9  8762  shftval  12907  sumeq1  13511  sumeq2w  13514  sumeq2ii  13515  zsum  13540  isumclim3  13574  isumshft  13651  prodeq1f  13715  prodeq2w  13719  prodeq2ii  13720  zprod  13744  iprodclim3  13793  pcval  14368  grpidval  15887  grpidpropd  15888  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  psgnfval  16525  psgnval  16532  psgndif  18638  dchrptlem1  23539  lgsdchrval  23622  ajval  25777  adjval  26809  resv1r  27827  bj-finsumval0  34663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250  df-iota 5556