Theorem ifid 4526

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

This proof depends on syntax axioms:   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  csbif  4543  rabsnif  4687  somincom  6132  fsuppmptif  9372  supsn  9446  infsn  9480  wemaplem2  9522  cantnflem1  9671  xrmaxeq  13233  xrmineq  13234  xaddpnf1  13280  xaddmnf1  13282  rexmul  13325  max0add  15399  sumz  15810  prod1  16035  1arithlem4  17022  xpscf  17655  mgm2nsgrplem2  19035  mgm2nsgrplem3  19036  dmdprdsplitlem  20170  fczpsrbag  22140  mplcoe1  22257  mplcoe3  22258  mplcoe5  22260  evlslem2  22299  mdet0  22832  mdetralt2  22835  mdetunilem9  22846  madurid  22870  decpmatid  22999  cnmpopc  25160  pcoval2  25248  pcorevlem  25258  itgz  26013  itgvallem3  26018  iblposlem  26024  iblss2  26038  itgss  26044  ditg0  26085  cnplimc  26119  limcco  26125  dvexp3  26210  ply1nzb  26353  plyeq0lem  26440  dgrcolem2  26504  plydivlem4  26530  radcnv0  26652  efrlim  27207  mumullem2  27417  lgsval2lem  27544  lgsdilem2  27570  fsuppind  43438  dgrsub2  43978  sqrtcval  44483  relexp1idm  44556  relexp0idm  44557