Theorem ifid 4527

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

Syntax hints:   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  csbif  4544  rabsnif  4688  somincom  6134  fsuppmptif  9358  supsn  9432  infsn  9466  wemaplem2  9508  cantnflem1  9657  xrmaxeq  13204  xrmineq  13205  xaddpnf1  13251  xaddmnf1  13253  rexmul  13296  max0add  15361  sumz  15773  prod1  15998  1arithlem4  16985  xpscf  17618  mgm2nsgrplem2  18980  mgm2nsgrplem3  18981  dmdprdsplitlem  20108  fczpsrbag  22050  mplcoe1  22167  mplcoe3  22168  mplcoe5  22170  evlslem2  22209  mdet0  22742  mdetralt2  22745  mdetunilem9  22756  madurid  22780  decpmatid  22906  cnmpopc  25066  pcoval2  25154  pcorevlem  25164  itgz  25919  itgvallem3  25924  iblposlem  25930  iblss2  25944  itgss  25950  ditg0  25991  cnplimc  26025  limcco  26031  dvexp3  26116  ply1nzb  26259  plyeq0lem  26346  dgrcolem2  26410  plydivlem4  26436  radcnv0  26555  efrlim  27110  mumullem2  27320  lgsval2lem  27447  lgsdilem2  27473  fsuppind  43292  dgrsub2  43832  sqrtcval  44337  relexp1idm  44410  relexp0idm  44411