| 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 7439 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵)) | |
| 2 | oveq2 7439 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶)) | |
| 3 | 1, 2 | ifsb 4539 | 1 ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ifcif 4525 (class class class)co 7431 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 |
| This theorem is referenced by: ramcl 17067 psrascl 21999 psdmvr 22173 matsc 22456 scmatscmide 22513 mulmarep1el 22578 maducoeval2 22646 madugsum 22649 itg2const 25775 itg2monolem1 25785 iblmulc2 25866 itgmulc2lem1 25867 bddmulibl 25874 dchrvmasumiflem2 27546 rpvmasum2 27556 sgnneg 34543 itg2addnclem 37678 itgaddnclem2 37686 itgmulc2nclem1 37693 readvrec 42392 selvvvval 42595 sqrtcval2 43655 |
| Copyright terms: Public domain | W3C validator |