Theorem ifid 4508

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

Syntax hints:   = wceq 1542  ifcif 4467

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 4468

This theorem is referenced by:  csbif  4525  rabsnif  4668  somincom  6098  fsuppmptif  9312  supsn  9386  infsn  9420  wemaplem2  9462  cantnflem1  9610  xrmaxeq  13131  xrmineq  13132  xaddpnf1  13178  xaddmnf1  13180  rexmul  13223  max0add  15272  sumz  15684  prod1  15909  1arithlem4  16897  xpscf  17529  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  dmdprdsplitlem  20014  fczpsrbag  21901  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  evlslem2  22057  mdet0  22571  mdetralt2  22574  mdetunilem9  22585  madurid  22609  decpmatid  22735  cnmpopc  24895  pcoval2  24983  pcorevlem  24993  itgz  25748  itgvallem3  25753  iblposlem  25759  iblss2  25773  itgss  25779  ditg0  25820  cnplimc  25854  limcco  25860  dvexp3  25945  ply1nzb  26088  plyeq0lem  26175  dgrcolem2  26239  plydivlem4  26262  radcnv0  26381  efrlim  26933  mumullem2  27143  lgsval2lem  27270  lgsdilem2  27296  fsuppind  43023  dgrsub2  43563  sqrtcval  44068  relexp1idm  44141  relexp0idm  44142