Theorem ifid 4465

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

Syntax hints:   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-if 4426

This theorem is referenced by:  csbif  4482  rabsnif  4625  somincom  5979  fsuppmptif  8993  supsn  9066  infsn  9099  wemaplem2  9141  cantnflem1  9282  xrmaxeq  12734  xrmineq  12735  xaddpnf1  12781  xaddmnf1  12783  rexmul  12826  max0add  14839  sumz  15251  prod1  15469  1arithlem4  16442  xpscf  17024  mgm2nsgrplem2  18300  mgm2nsgrplem3  18301  dmdprdsplitlem  19378  fczpsrbag  20836  mplcoe1  20948  mplcoe3  20949  mplcoe5  20951  evlslem2  20993  mdet0  21457  mdetralt2  21460  mdetunilem9  21471  madurid  21495  decpmatid  21621  cnmpopc  23779  pcoval2  23867  pcorevlem  23877  itgz  24632  itgvallem3  24637  iblposlem  24643  iblss2  24657  itgss  24663  ditg0  24704  cnplimc  24738  limcco  24744  dvexp3  24829  ply1nzb  24974  plyeq0lem  25058  dgrcolem2  25122  plydivlem4  25143  radcnv0  25262  efrlim  25806  mumullem2  26016  lgsval2lem  26142  lgsdilem2  26168  fsuppind  39930  dgrsub2  40604  sqrtcval  40866  relexp1idm  40940  relexp0idm  40941