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 7177 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐴 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐴𝐹𝐶)) | |
2 | oveq1 7177 | . 2 ⊢ (if(𝜑, 𝐴, 𝐵) = 𝐵 → (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = (𝐵𝐹𝐶)) | |
3 | 1, 2 | ifsb 4427 | 1 ⊢ (if(𝜑, 𝐴, 𝐵)𝐹𝐶) = if(𝜑, (𝐴𝐹𝐶), (𝐵𝐹𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ifcif 4414 (class class class)co 7170 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-iota 6297 df-fv 6347 df-ov 7173 |
This theorem is referenced by: scmatscm 21264 pmatcollpwscmatlem1 21540 idpm2idmp 21552 monmat2matmon 21575 chmatval 21580 leibpi 25680 musumsum 25929 muinv 25930 dchrinvcl 25989 rpvmasum2 26248 padicabvcxp 26368 pnfneige0 31473 plymulx0 32096 ftc1anclem6 35478 reabssgn 40789 sqrtcval 40794 linc0scn0 45298 |
Copyright terms: Public domain | W3C validator |