Theorem ifid 4541

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

Syntax hints:   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  csbif  4558  rabsnif  4699  somincom  6123  fsuppmptif  9411  supsn  9485  infsn  9519  wemaplem2  9561  cantnflem1  9703  xrmaxeq  13195  xrmineq  13196  xaddpnf1  13242  xaddmnf1  13244  rexmul  13287  max0add  15329  sumz  15738  prod1  15960  1arithlem4  16946  xpscf  17579  mgm2nsgrplem2  18897  mgm2nsgrplem3  18898  dmdprdsplitlem  20020  fczpsrbag  21881  mplcoe1  21995  mplcoe3  21996  mplcoe5  21998  evlslem2  22037  mdet0  22544  mdetralt2  22547  mdetunilem9  22558  madurid  22582  decpmatid  22708  cnmpopc  24873  pcoval2  24967  pcorevlem  24977  itgz  25734  itgvallem3  25739  iblposlem  25745  iblss2  25759  itgss  25765  ditg0  25806  cnplimc  25840  limcco  25846  dvexp3  25934  ply1nzb  26080  plyeq0lem  26167  dgrcolem2  26232  plydivlem4  26256  radcnv0  26377  efrlim  26931  efrlimOLD  26932  mumullem2  27142  lgsval2lem  27270  lgsdilem2  27296  fsuppind  42613  dgrsub2  43159  sqrtcval  43665  relexp1idm  43738  relexp0idm  43739