![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovif2 | Structured version Visualization version GIF version |
Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018.) |
Ref | Expression |
---|---|
ovif2 | ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 7364 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵)) | |
2 | oveq2 7364 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶)) | |
3 | 1, 2 | ifsb 4499 | 1 ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ifcif 4486 (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 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-iota 6448 df-fv 6504 df-ov 7359 |
This theorem is referenced by: ramcl 16900 matsc 21797 scmatscmide 21854 mulmarep1el 21919 maducoeval2 21987 madugsum 21990 itg2const 25103 itg2monolem1 25113 iblmulc2 25193 itgmulc2lem1 25194 bddmulibl 25201 dchrvmasumiflem2 26848 rpvmasum2 26858 sgnneg 33080 itg2addnclem 36119 itgaddnclem2 36127 itgmulc2nclem1 36134 mhphf 40748 sqrtcval2 41895 |
Copyright terms: Public domain | W3C validator |