Theorem ifid 4588

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

Syntax hints:   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  csbif  4605  rabsnif  4748  somincom  6166  fsuppmptif  9468  supsn  9541  infsn  9574  wemaplem2  9616  cantnflem1  9758  xrmaxeq  13241  xrmineq  13242  xaddpnf1  13288  xaddmnf1  13290  rexmul  13333  max0add  15359  sumz  15770  prod1  15992  1arithlem4  16973  xpscf  17625  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  dmdprdsplitlem  20081  fczpsrbag  21964  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  evlslem2  22126  mdet0  22633  mdetralt2  22636  mdetunilem9  22647  madurid  22671  decpmatid  22797  cnmpopc  24974  pcoval2  25068  pcorevlem  25078  itgz  25836  itgvallem3  25841  iblposlem  25847  iblss2  25861  itgss  25867  ditg0  25908  cnplimc  25942  limcco  25948  dvexp3  26036  ply1nzb  26182  plyeq0lem  26269  dgrcolem2  26334  plydivlem4  26356  radcnv0  26477  efrlim  27030  efrlimOLD  27031  mumullem2  27241  lgsval2lem  27369  lgsdilem2  27395  fsuppind  42545  dgrsub2  43092  sqrtcval  43603  relexp1idm  43676  relexp0idm  43677