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 182	1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴

Syntax hints:   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  csbif  4539  rabsnif  4682  somincom  6099  fsuppmptif  9314  supsn  9388  infsn  9422  wemaplem2  9464  cantnflem1  9610  xrmaxeq  13106  xrmineq  13107  xaddpnf1  13153  xaddmnf1  13155  rexmul  13198  max0add  15245  sumz  15657  prod1  15879  1arithlem4  16866  xpscf  17498  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  dmdprdsplitlem  19980  fczpsrbag  21889  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  evlslem2  22046  mdet0  22562  mdetralt2  22565  mdetunilem9  22576  madurid  22600  decpmatid  22726  cnmpopc  24890  pcoval2  24984  pcorevlem  24994  itgz  25750  itgvallem3  25755  iblposlem  25761  iblss2  25775  itgss  25781  ditg0  25822  cnplimc  25856  limcco  25862  dvexp3  25950  ply1nzb  26096  plyeq0lem  26183  dgrcolem2  26248  plydivlem4  26272  radcnv0  26393  efrlim  26947  efrlimOLD  26948  mumullem2  27158  lgsval2lem  27286  lgsdilem2  27312  fsuppind  42937  dgrsub2  43481  sqrtcval  43986  relexp1idm  44059  relexp0idm  44060