Theorem ifid 4521

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

Syntax hints:   = wceq 1542  ifcif 4480

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 4481

This theorem is referenced by:  csbif  4538  rabsnif  4681  somincom  6092  fsuppmptif  9306  supsn  9380  infsn  9414  wemaplem2  9456  cantnflem1  9602  xrmaxeq  13098  xrmineq  13099  xaddpnf1  13145  xaddmnf1  13147  rexmul  13190  max0add  15237  sumz  15649  prod1  15871  1arithlem4  16858  xpscf  17490  mgm2nsgrplem2  18848  mgm2nsgrplem3  18849  dmdprdsplitlem  19972  fczpsrbag  21881  mplcoe1  21996  mplcoe3  21997  mplcoe5  21999  evlslem2  22038  mdet0  22554  mdetralt2  22557  mdetunilem9  22568  madurid  22592  decpmatid  22718  cnmpopc  24882  pcoval2  24976  pcorevlem  24986  itgz  25742  itgvallem3  25747  iblposlem  25753  iblss2  25767  itgss  25773  ditg0  25814  cnplimc  25848  limcco  25854  dvexp3  25942  ply1nzb  26088  plyeq0lem  26175  dgrcolem2  26240  plydivlem4  26264  radcnv0  26385  efrlim  26939  efrlimOLD  26940  mumullem2  27150  lgsval2lem  27278  lgsdilem2  27304  fsuppind  42869  dgrsub2  43413  sqrtcval  43918  relexp1idm  43991  relexp0idm  43992