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

Theorem ovif2 7519
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 7428 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵))
2 oveq2 7428 . 2 (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶))
31, 2ifsb 4542 1 (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  ifcif 4529  (class class class)co 7420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423
This theorem is referenced by:  ramcl  16997  matsc  22351  scmatscmide  22408  mulmarep1el  22473  maducoeval2  22541  madugsum  22544  itg2const  25669  itg2monolem1  25679  iblmulc2  25759  itgmulc2lem1  25760  bddmulibl  25767  dchrvmasumiflem2  27434  rpvmasum2  27444  sgnneg  34160  itg2addnclem  37144  itgaddnclem2  37152  itgmulc2nclem1  37159  selvvvval  41818  sqrtcval2  43072
  Copyright terms: Public domain W3C validator