Theorem ifid 4571

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

Syntax hints:   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  csbif  4588  rabsnif  4728  somincom  6157  fsuppmptif  9437  supsn  9510  infsn  9543  wemaplem2  9585  cantnflem1  9727  xrmaxeq  13218  xrmineq  13219  xaddpnf1  13265  xaddmnf1  13267  rexmul  13310  max0add  15346  sumz  15755  prod1  15977  1arithlem4  16960  xpscf  17612  mgm2nsgrplem2  18945  mgm2nsgrplem3  18946  dmdprdsplitlem  20072  fczpsrbag  21959  mplcoe1  22073  mplcoe3  22074  mplcoe5  22076  evlslem2  22121  mdet0  22628  mdetralt2  22631  mdetunilem9  22642  madurid  22666  decpmatid  22792  cnmpopc  24969  pcoval2  25063  pcorevlem  25073  itgz  25831  itgvallem3  25836  iblposlem  25842  iblss2  25856  itgss  25862  ditg0  25903  cnplimc  25937  limcco  25943  dvexp3  26031  ply1nzb  26177  plyeq0lem  26264  dgrcolem2  26329  plydivlem4  26353  radcnv0  26474  efrlim  27027  efrlimOLD  27028  mumullem2  27238  lgsval2lem  27366  lgsdilem2  27392  fsuppind  42577  dgrsub2  43124  sqrtcval  43631  relexp1idm  43704  relexp0idm  43705