Theorem ifid 4158

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

Syntax hints:   = wceq 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  csbif  4171  rabsnif  4290  somincom  5565  fsuppmptif  8346  supsn  8419  infsn  8451  wemaplem2  8493  cantnflem1  8624  xrmaxeq  12048  xrmineq  12049  xaddpnf1  12095  xaddmnf1  12097  rexmul  12139  max0add  14094  sumz  14497  prod1  14718  1arithlem4  15677  xpscf  16273  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  dmdprdsplitlem  18482  fczpsrbag  19415  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  evlslem2  19560  mdet0  20460  mdetralt2  20463  mdetunilem9  20474  madurid  20498  decpmatid  20623  cnmpt2pc  22774  pcoval2  22862  pcorevlem  22872  itgz  23592  itgvallem3  23597  iblposlem  23603  iblss2  23617  itgss  23623  ditg0  23662  cnplimc  23696  limcco  23702  dvexp3  23786  ply1nzb  23927  plyeq0lem  24011  dgrcolem2  24075  plydivlem4  24096  radcnv0  24215  efrlim  24741  mumullem2  24951  lgsval2lem  25077  lgsdilem2  25103  dgrsub2  38022  relexp1idm  38323  relexp0idm  38324