Theorem fvif 5882

Description: Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.)

Assertion

Ref	Expression
fvif

Proof of Theorem fvif

Step	Hyp	Ref	Expression
1		fveq2 5871	. 2
2		fveq2 5871	. 2
3	1, 2	ifsb 3954	1

Syntax hints:  =wceq 1395  ifcif 3941  `cfv 5593

This theorem is referenced by:  ccatco  12801  sumeq2ii  13515  prodeq2ii  13720  ruclem1  13964  xpslem  14970  mat2pmat1  19233  decpmatid  19271  pmatcollpwscmatlem1  19290  copco  21518  pcopt  21522  pcopt2  21523  limccnp  22295  prmorcht  23452  pclogsum  23490  mblfinlem2  30052  ftc1anclem8  30097  ftc1anc  30098  fvifeq  32306

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-or 370  df-an 371  df-3an 975  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-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601