Theorem ifid 4517

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

Syntax hints:   = wceq 1540  ifcif 4476

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477

This theorem is referenced by:  csbif  4534  rabsnif  4675  somincom  6083  fsuppmptif  9289  supsn  9363  infsn  9397  wemaplem2  9439  cantnflem1  9585  xrmaxeq  13081  xrmineq  13082  xaddpnf1  13128  xaddmnf1  13130  rexmul  13173  max0add  15217  sumz  15629  prod1  15851  1arithlem4  16838  xpscf  17469  mgm2nsgrplem2  18793  mgm2nsgrplem3  18794  dmdprdsplitlem  19918  fczpsrbag  21828  mplcoe1  21942  mplcoe3  21943  mplcoe5  21945  evlslem2  21984  mdet0  22491  mdetralt2  22494  mdetunilem9  22505  madurid  22529  decpmatid  22655  cnmpopc  24820  pcoval2  24914  pcorevlem  24924  itgz  25680  itgvallem3  25685  iblposlem  25691  iblss2  25705  itgss  25711  ditg0  25752  cnplimc  25786  limcco  25792  dvexp3  25880  ply1nzb  26026  plyeq0lem  26113  dgrcolem2  26178  plydivlem4  26202  radcnv0  26323  efrlim  26877  efrlimOLD  26878  mumullem2  27088  lgsval2lem  27216  lgsdilem2  27242  fsuppind  42563  dgrsub2  43108  sqrtcval  43614  relexp1idm  43687  relexp0idm  43688