Theorem ifid 4075

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

Syntax hints:   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  csbif  4088  rabsnif  4202  somincom  5449  fsuppmptif  8188  supsn  8261  infsn  8293  wemaplem2  8335  cantnflem1  8469  xrmaxeq  11884  xrmineq  11885  xaddpnf1  11931  xaddmnf1  11933  rexmul  11973  max0add  13898  sumz  14300  prod1  14513  1arithlem4  15468  xpscf  16049  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  dmdprdsplitlem  18259  fczpsrbag  19188  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  evlslem2  19333  mdet0  20231  mdetralt2  20234  mdetunilem9  20245  madurid  20269  decpmatid  20394  cnmpt2pc  22535  pcoval2  22624  pcorevlem  22634  itgz  23353  itgvallem3  23358  iblposlem  23364  iblss2  23378  itgss  23384  ditg0  23423  cnplimc  23457  limcco  23463  dvexp3  23545  ply1nzb  23686  plyeq0lem  23770  dgrcolem2  23834  plydivlem4  23855  radcnv0  23974  efrlim  24496  mumullem2  24706  lgsval2lem  24832  lgsdilem2  24858  dgrsub2  36724  relexp1idm  37025  relexp0idm  37026