Theorem ifid 4506

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

Syntax hints:   = wceq 1537  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  csbif  4522  rabsnif  4659  somincom  5994  fsuppmptif  8863  supsn  8936  infsn  8969  wemaplem2  9011  cantnflem1  9152  xrmaxeq  12573  xrmineq  12574  xaddpnf1  12620  xaddmnf1  12622  rexmul  12665  max0add  14670  sumz  15079  prod1  15298  1arithlem4  16262  xpscf  16838  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  dmdprdsplitlem  19159  fczpsrbag  20147  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  evlslem2  20292  mdet0  21215  mdetralt2  21218  mdetunilem9  21229  madurid  21253  decpmatid  21378  cnmpopc  23532  pcoval2  23620  pcorevlem  23630  itgz  24381  itgvallem3  24386  iblposlem  24392  iblss2  24406  itgss  24412  ditg0  24451  cnplimc  24485  limcco  24491  dvexp3  24575  ply1nzb  24716  plyeq0lem  24800  dgrcolem2  24864  plydivlem4  24885  radcnv0  25004  efrlim  25547  mumullem2  25757  lgsval2lem  25883  lgsdilem2  25909  dgrsub2  39755  relexp1idm  40079  relexp0idm  40080