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

Syntax hints:   = wceq 1541  ifcif 4477

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4478

This theorem is referenced by:  csbif  4534  rabsnif  4675  somincom  6078  fsuppmptif  9260  supsn  9333  infsn  9366  wemaplem2  9408  cantnflem1  9550  xrmaxeq  13018  xrmineq  13019  xaddpnf1  13065  xaddmnf1  13067  rexmul  13110  max0add  15121  sumz  15533  prod1  15753  1arithlem4  16724  xpscf  17373  mgm2nsgrplem2  18654  mgm2nsgrplem3  18655  dmdprdsplitlem  19734  fczpsrbag  21231  mplcoe1  21343  mplcoe3  21344  mplcoe5  21346  evlslem2  21394  mdet0  21860  mdetralt2  21863  mdetunilem9  21874  madurid  21898  decpmatid  22024  cnmpopc  24196  pcoval2  24284  pcorevlem  24294  itgz  25050  itgvallem3  25055  iblposlem  25061  iblss2  25075  itgss  25081  ditg0  25122  cnplimc  25156  limcco  25162  dvexp3  25247  ply1nzb  25392  plyeq0lem  25476  dgrcolem2  25540  plydivlem4  25561  radcnv0  25680  efrlim  26224  mumullem2  26434  lgsval2lem  26560  lgsdilem2  26586  fsuppind  40590  dgrsub2  41274  sqrtcval  41622  relexp1idm  41695  relexp0idm  41696