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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  csbif  4543  rabsnif  4684  somincom  6140  fsuppmptif  9418  supsn  9492  infsn  9526  wemaplem2  9568  cantnflem1  9717  xrmaxeq  13336  xrmineq  13337  xaddpnf1  13383  xaddmnf1  13385  rexmul  13428  max0add  15506  sumz  15917  prod1  16140  1arithlem4  17133  xpscf  17766  mgm2nsgrplem2  19147  mgm2nsgrplem3  19148  dmdprdsplitlem  20283  fczpsrbag  22259  mplcoe1  22376  mplcoe3  22377  mplcoe5  22379  evlslem2  22418  mdet0  22951  mdetralt2  22954  mdetunilem9  22965  madurid  22989  decpmatid  23118  cnmpopc  25279  pcoval2  25367  pcorevlem  25377  itgz  26131  itgvallem3  26136  iblposlem  26142  iblss2  26156  itgss  26162  ditg0  26203  cnplimc  26237  limcco  26243  dvexp3  26328  ply1nzb  26471  plyeq0lem  26559  dgrcolem2  26623  plydivlem4  26647  radcnv0  26773  efrlim  27327  mumullem2  27537  lgsval2lem  27664  lgsdilem2  27690  fsuppind  43811  dgrsub2  44329  sqrtcval  44833  relexp1idm  44906  relexp0idm  44907