Theorem ifid 4515

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

Syntax hints:   = wceq 1554  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-if 4475

This theorem is referenced by:  csbif  4532  rabsnif  4676  somincom  6111  fsuppmptif  9335  supsn  9409  infsn  9443  wemaplem2  9485  cantnflem1  9634  xrmaxeq  13172  xrmineq  13173  xaddpnf1  13219  xaddmnf1  13221  rexmul  13264  max0add  15313  sumz  15725  prod1  15950  1arithlem4  16938  xpscf  17571  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  dmdprdsplitlem  20055  fczpsrbag  21946  mplcoe1  22063  mplcoe3  22064  mplcoe5  22066  evlslem2  22105  mdet0  22639  mdetralt2  22642  mdetunilem9  22653  madurid  22677  decpmatid  22803  cnmpopc  24963  pcoval2  25051  pcorevlem  25061  itgz  25816  itgvallem3  25821  iblposlem  25827  iblss2  25841  itgss  25847  ditg0  25888  cnplimc  25922  limcco  25928  dvexp3  26013  ply1nzb  26156  plyeq0lem  26243  dgrcolem2  26307  plydivlem4  26330  radcnv0  26449  efrlim  27004  mumullem2  27214  lgsval2lem  27341  lgsdilem2  27367  fsuppind  43120  dgrsub2  43660  sqrtcval  44165  relexp1idm  44238  relexp0idm  44239