![]() |
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 4492 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ifcif 4487 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3446 df-un 3916 df-if 4488 |
This theorem is referenced by: ifeq12d 4508 ifbieq2d 4513 ifeq2da 4519 ifcomnan 4543 rdgeq1 8358 cantnflem1d 9629 cantnflem1 9630 rexmul 13196 1arithlem4 16803 ramcl 16906 mplcoe1 21454 mplcoe5 21457 subrgascl 21490 selvffval 21542 selvval 21544 scmatscm 21878 marrepfval 21925 ma1repveval 21936 mulmarep1el 21937 mdetralt2 21974 mdetunilem8 21984 maduval 22003 maducoeval2 22005 madurid 22009 minmar1val0 22012 monmatcollpw 22144 pmatcollpwscmatlem1 22154 monmat2matmon 22189 itg2monolem1 25131 iblmulc2 25211 itgmulc2lem1 25212 bddmulibl 25219 dvtaylp 25745 dchrinvcl 26617 rpvmasum2 26876 padicfval 26980 plymulx 33217 itg2addnclem 36175 itg2addnclem3 36177 itg2addnc 36178 itgmulc2nclem1 36190 hdmap1fval 40305 cantnfresb 41702 itgioocnicc 44304 etransclem14 44575 etransclem17 44578 etransclem21 44582 etransclem25 44586 etransclem28 44589 etransclem31 44592 hsphoif 44903 hoidmvval 44904 hsphoival 44906 hoidmvlelem5 44926 hoidmvle 44927 ovnhoi 44930 hspmbllem2 44954 |
Copyright terms: Public domain | W3C validator |