![]() |
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 4232 | . 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴) | |
2 | iffalse 4235 | . 2 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴) | |
3 | 1, 2 | pm2.61i 176 | 1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ifcif 4226 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-if 4227 |
This theorem is referenced by: csbif 4278 rabsnif 4395 somincom 5670 fsuppmptif 8464 supsn 8537 infsn 8569 wemaplem2 8611 cantnflem1 8753 xrmaxeq 12214 xrmineq 12215 xaddpnf1 12261 xaddmnf1 12263 rexmul 12305 max0add 14257 sumz 14660 prod1 14880 1arithlem4 15836 xpscf 16433 mgm2nsgrplem2 17613 mgm2nsgrplem3 17614 dmdprdsplitlem 18643 fczpsrbag 19581 mplcoe1 19679 mplcoe3 19680 mplcoe5 19682 evlslem2 19726 mdet0 20629 mdetralt2 20632 mdetunilem9 20643 madurid 20667 decpmatid 20794 cnmpt2pc 22946 pcoval2 23034 pcorevlem 23044 itgz 23766 itgvallem3 23771 iblposlem 23777 iblss2 23791 itgss 23797 ditg0 23836 cnplimc 23870 limcco 23876 dvexp3 23960 ply1nzb 24101 plyeq0lem 24185 dgrcolem2 24249 plydivlem4 24270 radcnv0 24389 efrlim 24916 mumullem2 25126 lgsval2lem 25252 lgsdilem2 25278 dgrsub2 38231 relexp1idm 38532 relexp0idm 38533 |
Copyright terms: Public domain | W3C validator |