Theorem ifid 4529

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

Syntax hints:   = wceq 1540  ifcif 4488

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 4489

This theorem is referenced by:  csbif  4546  rabsnif  4687  somincom  6107  fsuppmptif  9350  supsn  9424  infsn  9458  wemaplem2  9500  cantnflem1  9642  xrmaxeq  13139  xrmineq  13140  xaddpnf1  13186  xaddmnf1  13188  rexmul  13231  max0add  15276  sumz  15688  prod1  15910  1arithlem4  16897  xpscf  17528  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  dmdprdsplitlem  19969  fczpsrbag  21830  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  evlslem2  21986  mdet0  22493  mdetralt2  22496  mdetunilem9  22507  madurid  22531  decpmatid  22657  cnmpopc  24822  pcoval2  24916  pcorevlem  24926  itgz  25682  itgvallem3  25687  iblposlem  25693  iblss2  25707  itgss  25713  ditg0  25754  cnplimc  25788  limcco  25794  dvexp3  25882  ply1nzb  26028  plyeq0lem  26115  dgrcolem2  26180  plydivlem4  26204  radcnv0  26325  efrlim  26879  efrlimOLD  26880  mumullem2  27090  lgsval2lem  27218  lgsdilem2  27244  fsuppind  42578  dgrsub2  43124  sqrtcval  43630  relexp1idm  43703  relexp0idm  43704