Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ifeq2d | Structured version Visualization version Unicode version |
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.) |
Ref | Expression |
---|---|
ifeq1d.1 |
Ref | Expression |
---|---|
ifeq2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifeq1d.1 | . 2 | |
2 | ifeq2 4091 | . 2 | |
3 | 1, 2 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 cif 4086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-un 3579 df-if 4087 |
This theorem is referenced by: ifeq12d 4106 ifbieq2d 4111 ifeq2da 4117 ifcomnan 4137 rdgeq1 7507 cantnflem1d 8585 cantnflem1 8586 rexmul 12101 1arithlem4 15630 ramcl 15733 mplcoe1 19465 mplcoe5 19468 subrgascl 19498 scmatscm 20319 marrepfval 20366 ma1repveval 20377 mulmarep1el 20378 mdetralt2 20415 mdetunilem8 20425 maduval 20444 maducoeval2 20446 madurid 20450 minmar1val0 20453 monmatcollpw 20584 pmatcollpwscmatlem1 20594 monmat2matmon 20629 itg2monolem1 23517 iblmulc2 23597 itgmulc2lem1 23598 bddmulibl 23605 dvtaylp 24124 dchrinvcl 24978 rpvmasum2 25201 padicfval 25305 plymulx 30625 itg2addnclem 33461 itg2addnclem3 33463 itg2addnc 33464 itgmulc2nclem1 33476 hdmap1fval 37086 itgioocnicc 40193 etransclem14 40465 etransclem17 40468 etransclem21 40472 etransclem25 40476 etransclem28 40479 etransclem31 40482 hsphoif 40790 hoidmvval 40791 hsphoival 40793 hoidmvlelem5 40813 hoidmvle 40814 ovnhoi 40817 hspmbllem2 40841 |
Copyright terms: Public domain | W3C validator |