Theorem ifid 4522

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

This proof depends on syntax axioms:   = wceq 1570  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  csbif  4539  rabsnif  4683  somincom  6122  fsuppmptif  9369  supsn  9443  infsn  9477  wemaplem2  9519  cantnflem1  9668  xrmaxeq  13279  xrmineq  13280  xaddpnf1  13326  xaddmnf1  13328  rexmul  13371  max0add  15445  sumz  15856  prod1  16079  1arithlem4  17066  xpscf  17699  mgm2nsgrplem2  19080  mgm2nsgrplem3  19081  dmdprdsplitlem  20215  fczpsrbag  22191  mplcoe1  22308  mplcoe3  22309  mplcoe5  22311  evlslem2  22350  mdet0  22883  mdetralt2  22886  mdetunilem9  22897  madurid  22921  decpmatid  23050  cnmpopc  25211  pcoval2  25299  pcorevlem  25309  itgz  26063  itgvallem3  26068  iblposlem  26074  iblss2  26088  itgss  26094  ditg0  26135  cnplimc  26169  limcco  26175  dvexp3  26260  ply1nzb  26403  plyeq0lem  26491  dgrcolem2  26555  plydivlem4  26581  radcnv0  26707  efrlim  27261  mumullem2  27471  lgsval2lem  27598  lgsdilem2  27624  fsuppind  43540  dgrsub2  44080  sqrtcval  44585  relexp1idm  44658  relexp0idm  44659