Theorem ifid 4527

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

This proof depends on syntax axioms:   = wceq 1569  ifcif 4486

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487

This theorem is used by:  csbif  4544  rabsnif  4688  somincom  6133  fsuppmptif  9357  supsn  9431  infsn  9465  wemaplem2  9507  cantnflem1  9656  xrmaxeq  13211  xrmineq  13212  xaddpnf1  13258  xaddmnf1  13260  rexmul  13303  max0add  15368  sumz  15780  prod1  16005  1arithlem4  16992  xpscf  17625  mgm2nsgrplem2  18987  mgm2nsgrplem3  18988  dmdprdsplitlem  20115  fczpsrbag  22082  mplcoe1  22199  mplcoe3  22200  mplcoe5  22202  evlslem2  22241  mdet0  22774  mdetralt2  22777  mdetunilem9  22788  madurid  22812  decpmatid  22938  cnmpopc  25098  pcoval2  25186  pcorevlem  25196  itgz  25951  itgvallem3  25956  iblposlem  25962  iblss2  25976  itgss  25982  ditg0  26023  cnplimc  26057  limcco  26063  dvexp3  26148  ply1nzb  26291  plyeq0lem  26378  dgrcolem2  26442  plydivlem4  26468  radcnv0  26590  efrlim  27145  mumullem2  27355  lgsval2lem  27482  lgsdilem2  27508  fsuppind  43350  dgrsub2  43890  sqrtcval  44395  relexp1idm  44468  relexp0idm  44469