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

Theorem ovif2 7456
Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018.)
Assertion
Ref Expression
ovif2 (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))

Proof of Theorem ovif2
StepHypRef Expression
1 oveq2 7366 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵))
2 oveq2 7366 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶))
31, 2ifsb 4500 1 (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  ifcif 4487  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  ramcl  16906  matsc  21815  scmatscmide  21872  mulmarep1el  21937  maducoeval2  22005  madugsum  22008  itg2const  25121  itg2monolem1  25131  iblmulc2  25211  itgmulc2lem1  25212  bddmulibl  25219  dchrvmasumiflem2  26866  rpvmasum2  26876  sgnneg  33197  itg2addnclem  36175  itgaddnclem2  36183  itgmulc2nclem1  36190  mhphf  40814  sqrtcval2  42002
  Copyright terms: Public domain W3C validator