Theorem ifid 4573

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

Syntax hints:   = wceq 1534  ifcif 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-if 4534

This theorem is referenced by:  csbif  4590  rabsnif  4732  somincom  6146  fsuppmptif  9442  supsn  9515  infsn  9548  wemaplem2  9590  cantnflem1  9732  xrmaxeq  13212  xrmineq  13213  xaddpnf1  13259  xaddmnf1  13261  rexmul  13304  max0add  15315  sumz  15726  prod1  15946  1arithlem4  16928  xpscf  17580  mgm2nsgrplem2  18909  mgm2nsgrplem3  18910  dmdprdsplitlem  20037  fczpsrbag  21920  mplcoe1  22044  mplcoe3  22045  mplcoe5  22047  evlslem2  22094  mdet0  22599  mdetralt2  22602  mdetunilem9  22613  madurid  22637  decpmatid  22763  cnmpopc  24940  pcoval2  25034  pcorevlem  25044  itgz  25801  itgvallem3  25806  iblposlem  25812  iblss2  25826  itgss  25832  ditg0  25873  cnplimc  25907  limcco  25913  dvexp3  26001  ply1nzb  26150  plyeq0lem  26237  dgrcolem2  26302  plydivlem4  26324  radcnv0  26445  efrlim  26997  efrlimOLD  26998  mumullem2  27208  lgsval2lem  27336  lgsdilem2  27362  fsuppind  42062  dgrsub2  42796  sqrtcval  43308  relexp1idm  43381  relexp0idm  43382