Theorem ifid 4519

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

Syntax hints:   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  csbif  4536  rabsnif  4677  somincom  6087  fsuppmptif  9308  supsn  9382  infsn  9416  wemaplem2  9458  cantnflem1  9604  xrmaxeq  13099  xrmineq  13100  xaddpnf1  13146  xaddmnf1  13148  rexmul  13191  max0add  15235  sumz  15647  prod1  15869  1arithlem4  16856  xpscf  17487  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  dmdprdsplitlem  19936  fczpsrbag  21846  mplcoe1  21960  mplcoe3  21961  mplcoe5  21963  evlslem2  22002  mdet0  22509  mdetralt2  22512  mdetunilem9  22523  madurid  22547  decpmatid  22673  cnmpopc  24838  pcoval2  24932  pcorevlem  24942  itgz  25698  itgvallem3  25703  iblposlem  25709  iblss2  25723  itgss  25729  ditg0  25770  cnplimc  25804  limcco  25810  dvexp3  25898  ply1nzb  26044  plyeq0lem  26131  dgrcolem2  26196  plydivlem4  26220  radcnv0  26341  efrlim  26895  efrlimOLD  26896  mumullem2  27106  lgsval2lem  27234  lgsdilem2  27260  fsuppind  42563  dgrsub2  43108  sqrtcval  43614  relexp1idm  43687  relexp0idm  43688