| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ifeq2d | Structured version Visualization version GIF version | ||
| Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
| Ref | Expression |
|---|---|
| ifeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| ifeq2d | ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ifeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 2 | ifeq2 4482 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1559 ifcif 4477 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-tru 1562 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-rab 3414 df-v 3455 df-un 3907 df-if 4478 |
| This theorem is referenced by: ifeq12d 4499 ifbieq2d 4504 ifeq2da 4510 ifcomnan 4534 rdgeq1 8376 cantnflem1d 9637 cantnflem1 9638 rexmul 13268 1arithlem4 16953 ramcl 17056 mplcoe1 22078 mplcoe5 22081 subrgascl 22107 selvffval 22159 selvval 22161 scmatscm 22561 marrepfval 22608 ma1repveval 22619 mulmarep1el 22620 mdetralt2 22657 mdetunilem8 22667 maduval 22686 maducoeval2 22688 madurid 22692 minmar1val0 22695 monmatcollpw 22827 pmatcollpwscmatlem1 22837 monmat2matmon 22872 itg2monolem1 25800 iblmulc2 25881 itgmulc2lem1 25882 bddmulibl 25889 plymulidp 26334 dvtaylp 26421 dchrinvcl 27305 rpvmasum2 27564 padicfval 27668 expsval 28506 itg2addnclem 38131 itg2addnclem3 38133 itg2addnc 38134 itgmulc2nclem1 38146 hdmap1fval 42381 cantnfresb 43862 itgioocnicc 46512 etransclem14 46783 etransclem17 46786 etransclem21 46790 etransclem25 46794 etransclem28 46797 etransclem31 46800 hsphoif 47111 hoidmvval 47112 hsphoival 47114 hoidmvlelem5 47134 hoidmvle 47135 ovnhoi 47138 hspmbllem2 47162 |
| Copyright terms: Public domain | W3C validator |