Theorem ifid 4383

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

Syntax hints:   = wceq 1507  ifcif 4344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-if 4345

This theorem is referenced by:  csbif  4399  rabsnif  4527  somincom  5828  fsuppmptif  8650  supsn  8723  infsn  8756  wemaplem2  8798  cantnflem1  8938  xrmaxeq  12382  xrmineq  12383  xaddpnf1  12429  xaddmnf1  12431  rexmul  12473  max0add  14521  sumz  14929  prod1  15148  1arithlem4  16108  xpscf  16685  mgm2nsgrplem2  17865  mgm2nsgrplem3  17866  dmdprdsplitlem  18899  fczpsrbag  19851  mplcoe1  19949  mplcoe3  19950  mplcoe5  19952  evlslem2  19995  mdet0  20909  mdetralt2  20912  mdetunilem9  20923  madurid  20947  decpmatid  21072  cnmpopc  23225  pcoval2  23313  pcorevlem  23323  itgz  24074  itgvallem3  24079  iblposlem  24085  iblss2  24099  itgss  24105  ditg0  24144  cnplimc  24178  limcco  24184  dvexp3  24268  ply1nzb  24409  plyeq0lem  24493  dgrcolem2  24557  plydivlem4  24578  radcnv0  24697  efrlim  25239  mumullem2  25449  lgsval2lem  25575  lgsdilem2  25601  dgrsub2  39076  relexp1idm  39367  relexp0idm  39368