Theorem ifid 4514

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

Syntax hints:   = wceq 1541  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4474

This theorem is referenced by:  csbif  4531  rabsnif  4674  somincom  6078  fsuppmptif  9278  supsn  9352  infsn  9386  wemaplem2  9428  cantnflem1  9574  xrmaxeq  13070  xrmineq  13071  xaddpnf1  13117  xaddmnf1  13119  rexmul  13162  max0add  15209  sumz  15621  prod1  15843  1arithlem4  16830  xpscf  17461  mgm2nsgrplem2  18819  mgm2nsgrplem3  18820  dmdprdsplitlem  19944  fczpsrbag  21851  mplcoe1  21965  mplcoe3  21966  mplcoe5  21968  evlslem2  22007  mdet0  22514  mdetralt2  22517  mdetunilem9  22528  madurid  22552  decpmatid  22678  cnmpopc  24842  pcoval2  24936  pcorevlem  24946  itgz  25702  itgvallem3  25707  iblposlem  25713  iblss2  25727  itgss  25733  ditg0  25774  cnplimc  25808  limcco  25814  dvexp3  25902  ply1nzb  26048  plyeq0lem  26135  dgrcolem2  26200  plydivlem4  26224  radcnv0  26345  efrlim  26899  efrlimOLD  26900  mumullem2  27110  lgsval2lem  27238  lgsdilem2  27264  fsuppind  42602  dgrsub2  43147  sqrtcval  43653  relexp1idm  43726  relexp0idm  43727