![]() |
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 4489 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ifcif 4484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3406 df-v 3445 df-un 3913 df-if 4485 |
This theorem is referenced by: ifeq12d 4505 ifbieq2d 4510 ifeq2da 4516 ifcomnan 4540 rdgeq1 8349 cantnflem1d 9582 cantnflem1 9583 rexmul 13144 1arithlem4 16758 ramcl 16861 mplcoe1 21390 mplcoe5 21393 subrgascl 21426 selvffval 21478 selvval 21480 scmatscm 21814 marrepfval 21861 ma1repveval 21872 mulmarep1el 21873 mdetralt2 21910 mdetunilem8 21920 maduval 21939 maducoeval2 21941 madurid 21945 minmar1val0 21948 monmatcollpw 22080 pmatcollpwscmatlem1 22090 monmat2matmon 22125 itg2monolem1 25067 iblmulc2 25147 itgmulc2lem1 25148 bddmulibl 25155 dvtaylp 25681 dchrinvcl 26553 rpvmasum2 26812 padicfval 26916 plymulx 32972 itg2addnclem 36067 itg2addnclem3 36069 itg2addnc 36070 itgmulc2nclem1 36082 hdmap1fval 40197 cantnfresb 41565 itgioocnicc 44119 etransclem14 44390 etransclem17 44393 etransclem21 44397 etransclem25 44401 etransclem28 44404 etransclem31 44407 hsphoif 44718 hoidmvval 44719 hsphoival 44721 hoidmvlelem5 44741 hoidmvle 44742 ovnhoi 44745 hspmbllem2 44769 |
Copyright terms: Public domain | W3C validator |