Theorem ovif2 7455

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 7364	. 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵))
2		oveq2 7364	. 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶))
3	1, 2	ifsb 4491	1 ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶))

Syntax hints:   = wceq 1541  ifcif 4477  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  ramcl  16955  psrascl  21932  psdmvr  22110  matsc  22392  scmatscmide  22449  mulmarep1el  22514  maducoeval2  22582  madugsum  22585  itg2const  25695  itg2monolem1  25705  iblmulc2  25786  itgmulc2lem1  25787  bddmulibl  25794  dchrvmasumiflem2  27467  rpvmasum2  27477  sgnneg  32863  itg2addnclem  37811  itgaddnclem2  37819  itgmulc2nclem1  37826  readvrec  42559  selvvvval  42770  sqrtcval2  43825