Theorem ifid 4568

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 4534	. 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
2		iffalse 4537	. 2 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐴) = 𝐴)
3	1, 2	pm2.61i 182	1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴

Syntax hints:   = wceq 1542  ifcif 4528

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  csbif  4585  rabsnif  4727  somincom  6133  fsuppmptif  9391  supsn  9464  infsn  9497  wemaplem2  9539  cantnflem1  9681  xrmaxeq  13155  xrmineq  13156  xaddpnf1  13202  xaddmnf1  13204  rexmul  13247  max0add  15254  sumz  15665  prod1  15885  1arithlem4  16856  xpscf  17508  mgm2nsgrplem2  18797  mgm2nsgrplem3  18798  dmdprdsplitlem  19902  fczpsrbag  21468  mplcoe1  21584  mplcoe3  21585  mplcoe5  21587  evlslem2  21634  mdet0  22100  mdetralt2  22103  mdetunilem9  22114  madurid  22138  decpmatid  22264  cnmpopc  24436  pcoval2  24524  pcorevlem  24534  itgz  25290  itgvallem3  25295  iblposlem  25301  iblss2  25315  itgss  25321  ditg0  25362  cnplimc  25396  limcco  25402  dvexp3  25487  ply1nzb  25632  plyeq0lem  25716  dgrcolem2  25780  plydivlem4  25801  radcnv0  25920  efrlim  26464  mumullem2  26674  lgsval2lem  26800  lgsdilem2  26826  fsuppind  41160  dgrsub2  41863  sqrtcval  42378  relexp1idm  42451  relexp0idm  42452