Theorem ifid 4532

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

Syntax hints:   = wceq 1540  ifcif 4491

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  csbif  4549  rabsnif  4690  somincom  6110  fsuppmptif  9357  supsn  9431  infsn  9465  wemaplem2  9507  cantnflem1  9649  xrmaxeq  13146  xrmineq  13147  xaddpnf1  13193  xaddmnf1  13195  rexmul  13238  max0add  15283  sumz  15695  prod1  15917  1arithlem4  16904  xpscf  17535  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  dmdprdsplitlem  19976  fczpsrbag  21837  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  evlslem2  21993  mdet0  22500  mdetralt2  22503  mdetunilem9  22514  madurid  22538  decpmatid  22664  cnmpopc  24829  pcoval2  24923  pcorevlem  24933  itgz  25689  itgvallem3  25694  iblposlem  25700  iblss2  25714  itgss  25720  ditg0  25761  cnplimc  25795  limcco  25801  dvexp3  25889  ply1nzb  26035  plyeq0lem  26122  dgrcolem2  26187  plydivlem4  26211  radcnv0  26332  efrlim  26886  efrlimOLD  26887  mumullem2  27097  lgsval2lem  27225  lgsdilem2  27251  fsuppind  42585  dgrsub2  43131  sqrtcval  43637  relexp1idm  43710  relexp0idm  43711