Theorem ifid 4502

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

Syntax hints:   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  csbif  4519  rabsnif  4662  somincom  6091  fsuppmptif  9309  supsn  9383  infsn  9417  wemaplem2  9459  cantnflem1  9608  xrmaxeq  13129  xrmineq  13130  xaddpnf1  13176  xaddmnf1  13178  rexmul  13221  max0add  15270  sumz  15682  prod1  15907  1arithlem4  16895  xpscf  17527  mgm2nsgrplem2  18888  mgm2nsgrplem3  18889  dmdprdsplitlem  20012  fczpsrbag  21903  mplcoe1  22020  mplcoe3  22021  mplcoe5  22023  evlslem2  22062  mdet0  22596  mdetralt2  22599  mdetunilem9  22610  madurid  22634  decpmatid  22760  cnmpopc  24920  pcoval2  25008  pcorevlem  25018  itgz  25773  itgvallem3  25778  iblposlem  25784  iblss2  25798  itgss  25804  ditg0  25845  cnplimc  25879  limcco  25885  dvexp3  25970  ply1nzb  26113  plyeq0lem  26200  dgrcolem2  26264  plydivlem4  26287  radcnv0  26406  efrlim  26958  mumullem2  27168  lgsval2lem  27295  lgsdilem2  27321  fsuppind  43041  dgrsub2  43581  sqrtcval  44086  relexp1idm  44159  relexp0idm  44160