Theorem ifid 4506

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

Syntax hints:   = wceq 1533  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  csbif  4522  rabsnif  4653  somincom  5989  fsuppmptif  8857  supsn  8930  infsn  8963  wemaplem2  9005  cantnflem1  9146  xrmaxeq  12566  xrmineq  12567  xaddpnf1  12613  xaddmnf1  12615  rexmul  12658  max0add  14664  sumz  15073  prod1  15292  1arithlem4  16256  xpscf  16832  mgm2nsgrplem2  18078  mgm2nsgrplem3  18079  dmdprdsplitlem  19153  fczpsrbag  20141  mplcoe1  20240  mplcoe3  20241  mplcoe5  20243  evlslem2  20286  mdet0  21209  mdetralt2  21212  mdetunilem9  21223  madurid  21247  decpmatid  21372  cnmpopc  23526  pcoval2  23614  pcorevlem  23624  itgz  24375  itgvallem3  24380  iblposlem  24386  iblss2  24400  itgss  24406  ditg0  24445  cnplimc  24479  limcco  24485  dvexp3  24569  ply1nzb  24710  plyeq0lem  24794  dgrcolem2  24858  plydivlem4  24879  radcnv0  24998  efrlim  25541  mumullem2  25751  lgsval2lem  25877  lgsdilem2  25903  dgrsub2  39728  relexp1idm  40052  relexp0idm  40053