Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvif Unicode version

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
StepHypRef Expression
1 fveq2 5871 . 2
2 fveq2 5871 . 2
31, 2ifsb 3954 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator