Theorem ovif2 7458

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

Step	Hyp	Ref	Expression
1		oveq2 7367	. 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵))
2		oveq2 7367	. 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶))
3	1, 2	ifsb 4470	1 ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))

Syntax hints:   = wceq 1548  ifcif 4456  (class class class)co 7359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6444  df-fv 6496  df-ov 7362

This theorem is referenced by:  ramcl  16995  psrascl  21956  selvvvval  22121  psdmvr  22160  matsc  22436  scmatscmide  22493  mulmarep1el  22558  maducoeval2  22626  madugsum  22629  itg2const  25728  itg2monolem1  25738  iblmulc2  25819  itgmulc2lem1  25820  bddmulibl  25827  dchrvmasumiflem2  27486  rpvmasum2  27496  sgnneg  32927  itg2addnclem  38051  itgaddnclem2  38059  itgmulc2nclem1  38066  readvrec  42852  sqrtcval2  44099