![]() |
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 4535 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ifcif 4530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-un 3949 df-if 4531 |
This theorem is referenced by: ifeq12d 4551 ifbieq2d 4556 ifeq2da 4562 ifcomnan 4586 rdgeq1 8432 cantnflem1d 9713 cantnflem1 9714 rexmul 13285 1arithlem4 16898 ramcl 17001 mplcoe1 21997 mplcoe5 22000 subrgascl 22032 selvffval 22081 selvval 22083 scmatscm 22459 marrepfval 22506 ma1repveval 22517 mulmarep1el 22518 mdetralt2 22555 mdetunilem8 22565 maduval 22584 maducoeval2 22586 madurid 22590 minmar1val0 22593 monmatcollpw 22725 pmatcollpwscmatlem1 22735 monmat2matmon 22770 itg2monolem1 25724 iblmulc2 25804 itgmulc2lem1 25805 bddmulibl 25812 dvtaylp 26350 dchrinvcl 27231 rpvmasum2 27490 padicfval 27594 plymulx 34311 itg2addnclem 37275 itg2addnclem3 37277 itg2addnc 37278 itgmulc2nclem1 37290 hdmap1fval 41399 cantnfresb 42895 itgioocnicc 45503 etransclem14 45774 etransclem17 45777 etransclem21 45781 etransclem25 45785 etransclem28 45788 etransclem31 45791 hsphoif 46102 hoidmvval 46103 hsphoival 46105 hoidmvlelem5 46125 hoidmvle 46126 ovnhoi 46129 hspmbllem2 46153 |
Copyright terms: Public domain | W3C validator |