Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ovif | Structured version Visualization version GIF version |
Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
Ref | Expression |
---|---|
ovif | ⊢ (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 7282 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐴𝐹𝐶)) | |
2 | oveq1 7282 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐵𝐹𝐶)) | |
3 | 1, 2 | ifsb 4472 | 1 ⊢ (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ifcif 4459 (class class class)co 7275 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-iota 6391 df-fv 6441 df-ov 7278 |
This theorem is referenced by: scmatscm 21662 pmatcollpwscmatlem1 21938 idpm2idmp 21950 monmat2matmon 21973 chmatval 21978 leibpi 26092 musumsum 26341 muinv 26342 dchrinvcl 26401 rpvmasum2 26660 padicabvcxp 26780 pnfneige0 31901 plymulx0 32526 ftc1anclem6 35855 reabssgn 41244 sqrtcval 41249 linc0scn0 45764 |
Copyright terms: Public domain | W3C validator |