MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifid Structured version   Visualization version   GIF version

Theorem ifid 4102
Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
Assertion
Ref Expression
ifid if(𝜑, 𝐴, 𝐴) = 𝐴

Proof of Theorem ifid
StepHypRef Expression
1 iftrue 4069 . 2 (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
2 iffalse 4072 . 2 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
31, 2pm2.61i 176 1 if(𝜑, 𝐴, 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4064
This theorem is referenced by:  csbif  4115  rabsnif  4233  somincom  5494  fsuppmptif  8256  supsn  8329  infsn  8361  wemaplem2  8403  cantnflem1  8537  xrmaxeq  11960  xrmineq  11961  xaddpnf1  12007  xaddmnf1  12009  rexmul  12051  max0add  13991  sumz  14393  prod1  14606  1arithlem4  15561  xpscf  16154  mgm2nsgrplem2  17334  mgm2nsgrplem3  17335  dmdprdsplitlem  18364  fczpsrbag  19295  mplcoe1  19393  mplcoe3  19394  mplcoe5  19396  evlslem2  19440  mdet0  20340  mdetralt2  20343  mdetunilem9  20354  madurid  20378  decpmatid  20503  cnmpt2pc  22646  pcoval2  22735  pcorevlem  22745  itgz  23466  itgvallem3  23471  iblposlem  23477  iblss2  23491  itgss  23497  ditg0  23536  cnplimc  23570  limcco  23576  dvexp3  23658  ply1nzb  23799  plyeq0lem  23883  dgrcolem2  23947  plydivlem4  23968  radcnv0  24087  efrlim  24609  mumullem2  24819  lgsval2lem  24945  lgsdilem2  24971  dgrsub2  37213  relexp1idm  37514  relexp0idm  37515
  Copyright terms: Public domain W3C validator