Theorem ovif2 7468

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

Syntax hints:   = wceq 1540  ifcif 4484  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  ramcl  16976  psrascl  21921  psdmvr  22089  matsc  22370  scmatscmide  22427  mulmarep1el  22492  maducoeval2  22560  madugsum  22563  itg2const  25674  itg2monolem1  25684  iblmulc2  25765  itgmulc2lem1  25766  bddmulibl  25773  dchrvmasumiflem2  27446  rpvmasum2  27456  sgnneg  32808  itg2addnclem  37658  itgaddnclem2  37666  itgmulc2nclem1  37673  readvrec  42343  selvvvval  42566  sqrtcval2  43624