Theorem ifid 4508

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 182	1 ⊢ if(𝜑, 𝐴, 𝐴) = 𝐴

Syntax hints:   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  csbif  4525  rabsnif  4668  somincom  6089  fsuppmptif  9303  supsn  9377  infsn  9411  wemaplem2  9453  cantnflem1  9599  xrmaxeq  13120  xrmineq  13121  xaddpnf1  13167  xaddmnf1  13169  rexmul  13212  max0add  15261  sumz  15673  prod1  15898  1arithlem4  16886  xpscf  17518  mgm2nsgrplem2  18879  mgm2nsgrplem3  18880  dmdprdsplitlem  20003  fczpsrbag  21909  mplcoe1  22024  mplcoe3  22025  mplcoe5  22027  evlslem2  22066  mdet0  22580  mdetralt2  22583  mdetunilem9  22594  madurid  22618  decpmatid  22744  cnmpopc  24904  pcoval2  24992  pcorevlem  25002  itgz  25757  itgvallem3  25762  iblposlem  25768  iblss2  25782  itgss  25788  ditg0  25829  cnplimc  25863  limcco  25869  dvexp3  25954  ply1nzb  26100  plyeq0lem  26187  dgrcolem2  26251  plydivlem4  26275  radcnv0  26396  efrlim  26950  efrlimOLD  26951  mumullem2  27161  lgsval2lem  27289  lgsdilem2  27315  fsuppind  43034  dgrsub2  43578  sqrtcval  44083  relexp1idm  44156  relexp0idm  44157