Theorem ifid 4524

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

Syntax hints:   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  csbif  4541  rabsnif  4685  somincom  6125  fsuppmptif  9347  supsn  9421  infsn  9455  wemaplem2  9497  cantnflem1  9646  xrmaxeq  13196  xrmineq  13197  xaddpnf1  13243  xaddmnf1  13245  rexmul  13288  max0add  15351  sumz  15763  prod1  15988  1arithlem4  16976  xpscf  17609  mgm2nsgrplem2  18971  mgm2nsgrplem3  18972  dmdprdsplitlem  20100  fczpsrbag  22031  mplcoe1  22148  mplcoe3  22149  mplcoe5  22151  evlslem2  22190  mdet0  22724  mdetralt2  22727  mdetunilem9  22738  madurid  22762  decpmatid  22888  cnmpopc  25048  pcoval2  25136  pcorevlem  25146  itgz  25901  itgvallem3  25906  iblposlem  25912  iblss2  25926  itgss  25932  ditg0  25973  cnplimc  26007  limcco  26013  dvexp3  26098  ply1nzb  26241  plyeq0lem  26328  dgrcolem2  26392  plydivlem4  26418  radcnv0  26537  efrlim  27092  mumullem2  27302  lgsval2lem  27429  lgsdilem2  27455  fsuppind  43184  dgrsub2  43724  sqrtcval  44229  relexp1idm  44302  relexp0idm  44303