Theorem ifid 4511

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

Syntax hints:   = wceq 1550  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-if 4471

This theorem is referenced by:  csbif  4528  rabsnif  4672  somincom  6107  fsuppmptif  9331  supsn  9405  infsn  9439  wemaplem2  9481  cantnflem1  9630  xrmaxeq  13168  xrmineq  13169  xaddpnf1  13215  xaddmnf1  13217  rexmul  13260  max0add  15309  sumz  15721  prod1  15946  1arithlem4  16934  xpscf  17567  mgm2nsgrplem2  18928  mgm2nsgrplem3  18929  dmdprdsplitlem  20051  fczpsrbag  21942  mplcoe1  22059  mplcoe3  22060  mplcoe5  22062  evlslem2  22101  mdet0  22635  mdetralt2  22638  mdetunilem9  22649  madurid  22673  decpmatid  22799  cnmpopc  24959  pcoval2  25047  pcorevlem  25057  itgz  25812  itgvallem3  25817  iblposlem  25823  iblss2  25837  itgss  25843  ditg0  25884  cnplimc  25918  limcco  25924  dvexp3  26009  ply1nzb  26152  plyeq0lem  26239  dgrcolem2  26303  plydivlem4  26326  radcnv0  26445  efrlim  27000  mumullem2  27210  lgsval2lem  27337  lgsdilem2  27363  fsuppind  43110  dgrsub2  43650  sqrtcval  44155  relexp1idm  44228  relexp0idm  44229