Theorem ifid 4265

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

Syntax hints:   = wceq 1631  ifcif 4226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4227

This theorem is referenced by:  csbif  4278  rabsnif  4395  somincom  5670  fsuppmptif  8464  supsn  8537  infsn  8569  wemaplem2  8611  cantnflem1  8753  xrmaxeq  12214  xrmineq  12215  xaddpnf1  12261  xaddmnf1  12263  rexmul  12305  max0add  14257  sumz  14660  prod1  14880  1arithlem4  15836  xpscf  16433  mgm2nsgrplem2  17613  mgm2nsgrplem3  17614  dmdprdsplitlem  18643  fczpsrbag  19581  mplcoe1  19679  mplcoe3  19680  mplcoe5  19682  evlslem2  19726  mdet0  20629  mdetralt2  20632  mdetunilem9  20643  madurid  20667  decpmatid  20794  cnmpt2pc  22946  pcoval2  23034  pcorevlem  23044  itgz  23766  itgvallem3  23771  iblposlem  23777  iblss2  23791  itgss  23797  ditg0  23836  cnplimc  23870  limcco  23876  dvexp3  23960  ply1nzb  24101  plyeq0lem  24185  dgrcolem2  24249  plydivlem4  24270  radcnv0  24389  efrlim  24916  mumullem2  25126  lgsval2lem  25252  lgsdilem2  25278  dgrsub2  38231  relexp1idm  38532  relexp0idm  38533