Theorem ifid 4496

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

Syntax hints:   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  csbif  4513  rabsnif  4656  somincom  6028  fsuppmptif  9088  supsn  9161  infsn  9194  wemaplem2  9236  cantnflem1  9377  xrmaxeq  12842  xrmineq  12843  xaddpnf1  12889  xaddmnf1  12891  rexmul  12934  max0add  14950  sumz  15362  prod1  15582  1arithlem4  16555  xpscf  17193  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  dmdprdsplitlem  19555  fczpsrbag  21036  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  evlslem2  21199  mdet0  21663  mdetralt2  21666  mdetunilem9  21677  madurid  21701  decpmatid  21827  cnmpopc  23997  pcoval2  24085  pcorevlem  24095  itgz  24850  itgvallem3  24855  iblposlem  24861  iblss2  24875  itgss  24881  ditg0  24922  cnplimc  24956  limcco  24962  dvexp3  25047  ply1nzb  25192  plyeq0lem  25276  dgrcolem2  25340  plydivlem4  25361  radcnv0  25480  efrlim  26024  mumullem2  26234  lgsval2lem  26360  lgsdilem2  26386  fsuppind  40202  dgrsub2  40876  sqrtcval  41138  relexp1idm  41211  relexp0idm  41212