Theorem ifid 4517

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

Syntax hints:   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  csbif  4534  rabsnif  4677  somincom  6088  fsuppmptif  9293  supsn  9367  infsn  9401  wemaplem2  9443  cantnflem1  9589  xrmaxeq  13088  xrmineq  13089  xaddpnf1  13135  xaddmnf1  13137  rexmul  13180  max0add  15227  sumz  15639  prod1  15861  1arithlem4  16848  xpscf  17479  mgm2nsgrplem2  18837  mgm2nsgrplem3  18838  dmdprdsplitlem  19961  fczpsrbag  21868  mplcoe1  21982  mplcoe3  21983  mplcoe5  21985  evlslem2  22024  mdet0  22531  mdetralt2  22534  mdetunilem9  22545  madurid  22569  decpmatid  22695  cnmpopc  24859  pcoval2  24953  pcorevlem  24963  itgz  25719  itgvallem3  25724  iblposlem  25730  iblss2  25744  itgss  25750  ditg0  25791  cnplimc  25825  limcco  25831  dvexp3  25919  ply1nzb  26065  plyeq0lem  26152  dgrcolem2  26217  plydivlem4  26241  radcnv0  26362  efrlim  26916  efrlimOLD  26917  mumullem2  27127  lgsval2lem  27255  lgsdilem2  27281  fsuppind  42698  dgrsub2  43242  sqrtcval  43748  relexp1idm  43821  relexp0idm  43822