![]() |
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 4312 | . 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ifcif 4307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-un 3797 df-if 4308 |
This theorem is referenced by: ifeq12d 4327 ifbieq2d 4332 ifeq2da 4338 ifcomnan 4361 rdgeq1 7792 cantnflem1d 8884 cantnflem1 8885 rexmul 12417 1arithlem4 16038 ramcl 16141 mplcoe1 19866 mplcoe5 19869 subrgascl 19898 scmatscm 20728 marrepfval 20775 ma1repveval 20786 mulmarep1el 20787 mdetralt2 20824 mdetunilem8 20834 maduval 20853 maducoeval2 20855 madurid 20859 minmar1val0 20862 monmatcollpw 20995 pmatcollpwscmatlem1 21005 monmat2matmon 21040 itg2monolem1 23958 iblmulc2 24038 itgmulc2lem1 24039 bddmulibl 24046 dvtaylp 24565 dchrinvcl 25434 rpvmasum2 25657 padicfval 25761 plymulx 31229 itg2addnclem 34091 itg2addnclem3 34093 itg2addnc 34094 itgmulc2nclem1 34106 hdmap1fval 37955 itgioocnicc 41130 etransclem14 41402 etransclem17 41405 etransclem21 41409 etransclem25 41413 etransclem28 41416 etransclem31 41419 hsphoif 41727 hoidmvval 41728 hsphoival 41730 hoidmvlelem5 41750 hoidmvle 41751 ovnhoi 41754 hspmbllem2 41778 |
Copyright terms: Public domain | W3C validator |