![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifid | Structured version Visualization version GIF version |
Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.) |
Ref | Expression |
---|---|
ifid | ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 4350 | . 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴) | |
2 | iffalse 4353 | . 2 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴) | |
3 | 1, 2 | pm2.61i 177 | 1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ifcif 4344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-ex 1743 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-if 4345 |
This theorem is referenced by: csbif 4399 rabsnif 4527 somincom 5828 fsuppmptif 8650 supsn 8723 infsn 8756 wemaplem2 8798 cantnflem1 8938 xrmaxeq 12382 xrmineq 12383 xaddpnf1 12429 xaddmnf1 12431 rexmul 12473 max0add 14521 sumz 14929 prod1 15148 1arithlem4 16108 xpscf 16685 mgm2nsgrplem2 17865 mgm2nsgrplem3 17866 dmdprdsplitlem 18899 fczpsrbag 19851 mplcoe1 19949 mplcoe3 19950 mplcoe5 19952 evlslem2 19995 mdet0 20909 mdetralt2 20912 mdetunilem9 20923 madurid 20947 decpmatid 21072 cnmpopc 23225 pcoval2 23313 pcorevlem 23323 itgz 24074 itgvallem3 24079 iblposlem 24085 iblss2 24099 itgss 24105 ditg0 24144 cnplimc 24178 limcco 24184 dvexp3 24268 ply1nzb 24409 plyeq0lem 24493 dgrcolem2 24557 plydivlem4 24578 radcnv0 24697 efrlim 25239 mumullem2 25449 lgsval2lem 25575 lgsdilem2 25601 dgrsub2 39076 relexp1idm 39367 relexp0idm 39368 |
Copyright terms: Public domain | W3C validator |