![]() |
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 7456 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐵 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐵)) | |
2 | oveq2 7456 | . 2 ⊢ (if(𝜑, 𝐵, 𝐶) = 𝐶 → (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = (𝐴𝐹𝐶)) | |
3 | 1, 2 | ifsb 4561 | 1 ⊢ (𝐴𝐹if(𝜑, 𝐵, 𝐶)) = if(𝜑, (𝐴𝐹𝐵), (𝐴𝐹𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ifcif 4548 (class class class)co 7448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-iota 6525 df-fv 6581 df-ov 7451 |
This theorem is referenced by: ramcl 17076 psrascl 22022 matsc 22477 scmatscmide 22534 mulmarep1el 22599 maducoeval2 22667 madugsum 22670 itg2const 25795 itg2monolem1 25805 iblmulc2 25886 itgmulc2lem1 25887 bddmulibl 25894 dchrvmasumiflem2 27564 rpvmasum2 27574 sgnneg 34505 itg2addnclem 37631 itgaddnclem2 37639 itgmulc2nclem1 37646 selvvvval 42540 sqrtcval2 43604 |
Copyright terms: Public domain | W3C validator |