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 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  csbif  4539  rabsnif  4683  somincom  6127  fsuppmptif  9392  supsn  9466  infsn  9500  wemaplem2  9542  cantnflem1  9691  xrmaxeq  13310  xrmineq  13311  xaddpnf1  13357  xaddmnf1  13359  rexmul  13402  max0add  15478  sumz  15889  prod1  16112  1arithlem4  17105  xpscf  17738  mgm2nsgrplem2  19119  mgm2nsgrplem3  19120  dmdprdsplitlem  20254  fczpsrbag  22230  mplcoe1  22347  mplcoe3  22348  mplcoe5  22350  evlslem2  22389  mdet0  22922  mdetralt2  22925  mdetunilem9  22936  madurid  22960  decpmatid  23089  cnmpopc  25250  pcoval2  25338  pcorevlem  25348  itgz  26102  itgvallem3  26107  iblposlem  26113  iblss2  26127  itgss  26133  ditg0  26174  cnplimc  26208  limcco  26214  dvexp3  26299  ply1nzb  26442  plyeq0lem  26530  dgrcolem2  26594  plydivlem4  26618  radcnv0  26744  efrlim  27298  mumullem2  27508  lgsval2lem  27635  lgsdilem2  27661  fsuppind  43694  dgrsub2  44213  sqrtcval  44717  relexp1idm  44790  relexp0idm  44791