Theorem ifid 4500

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

Step	Hyp	Ref	Expression
1		iftrue 4466	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
2		iffalse 4469	. 2 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
3	1, 2	pm2.61i 182	1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴

Syntax hints:   = wceq 1539  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  csbif  4517  rabsnif  4660  somincom  6044  fsuppmptif  9167  supsn  9240  infsn  9273  wemaplem2  9315  cantnflem1  9456  xrmaxeq  12922  xrmineq  12923  xaddpnf1  12969  xaddmnf1  12971  rexmul  13014  max0add  15031  sumz  15443  prod1  15663  1arithlem4  16636  xpscf  17285  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  dmdprdsplitlem  19649  fczpsrbag  21135  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  evlslem2  21298  mdet0  21764  mdetralt2  21767  mdetunilem9  21778  madurid  21802  decpmatid  21928  cnmpopc  24100  pcoval2  24188  pcorevlem  24198  itgz  24954  itgvallem3  24959  iblposlem  24965  iblss2  24979  itgss  24985  ditg0  25026  cnplimc  25060  limcco  25066  dvexp3  25151  ply1nzb  25296  plyeq0lem  25380  dgrcolem2  25444  plydivlem4  25465  radcnv0  25584  efrlim  26128  mumullem2  26338  lgsval2lem  26464  lgsdilem2  26490  fsuppind  40286  dgrsub2  40967  sqrtcval  41256  relexp1idm  41329  relexp0idm  41330