Theorem ifid 4569

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

Syntax hints:   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  csbif  4586  rabsnif  4728  somincom  6136  fsuppmptif  9394  supsn  9467  infsn  9500  wemaplem2  9542  cantnflem1  9684  xrmaxeq  13158  xrmineq  13159  xaddpnf1  13205  xaddmnf1  13207  rexmul  13250  max0add  15257  sumz  15668  prod1  15888  1arithlem4  16859  xpscf  17511  mgm2nsgrplem2  18800  mgm2nsgrplem3  18801  dmdprdsplitlem  19907  fczpsrbag  21476  mplcoe1  21592  mplcoe3  21593  mplcoe5  21595  evlslem2  21642  mdet0  22108  mdetralt2  22111  mdetunilem9  22122  madurid  22146  decpmatid  22272  cnmpopc  24444  pcoval2  24532  pcorevlem  24542  itgz  25298  itgvallem3  25303  iblposlem  25309  iblss2  25323  itgss  25329  ditg0  25370  cnplimc  25404  limcco  25410  dvexp3  25495  ply1nzb  25640  plyeq0lem  25724  dgrcolem2  25788  plydivlem4  25809  radcnv0  25928  efrlim  26474  mumullem2  26684  lgsval2lem  26810  lgsdilem2  26836  fsuppind  41162  dgrsub2  41877  sqrtcval  42392  relexp1idm  42465  relexp0idm  42466