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

Theorem ovif2 6380
 Description: Move a conditional outside of an operation (Contributed by Thierry Arnoux, 1-Oct-2018.)
Assertion
Ref Expression
ovif2

Proof of Theorem ovif2
StepHypRef Expression
1 oveq2 6304 . 2
2 oveq2 6304 . 2
31, 2ifsb 3954 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  ifcif 3941  (class class class)co 6296 This theorem is referenced by:  ramcl  14547  matsc  18952  scmatscmide  19009  mulmarep1el  19074  maducoeval2  19142  madugsum  19145  itg2const  22147  itg2monolem1  22157  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  dchrvmasumiflem2  23687  rpvmasum2  23697  sgnneg  28479  itg2addnclem  30066  itgaddnclem2  30074  itgmulc2nclem1  30081 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  df-ov 6299
 Copyright terms: Public domain W3C validator