Theorem ifid 4125

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

Syntax hints:   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  csbif  4138  rabsnif  4258  somincom  5530  fsuppmptif  8305  supsn  8378  infsn  8410  wemaplem2  8452  cantnflem1  8586  xrmaxeq  12010  xrmineq  12011  xaddpnf1  12057  xaddmnf1  12059  rexmul  12101  max0add  14050  sumz  14453  prod1  14674  1arithlem4  15630  xpscf  16226  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  dmdprdsplitlem  18436  fczpsrbag  19367  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  evlslem2  19512  mdet0  20412  mdetralt2  20415  mdetunilem9  20426  madurid  20450  decpmatid  20575  cnmpt2pc  22727  pcoval2  22816  pcorevlem  22826  itgz  23547  itgvallem3  23552  iblposlem  23558  iblss2  23572  itgss  23578  ditg0  23617  cnplimc  23651  limcco  23657  dvexp3  23741  ply1nzb  23882  plyeq0lem  23966  dgrcolem2  24030  plydivlem4  24051  radcnv0  24170  efrlim  24696  mumullem2  24906  lgsval2lem  25032  lgsdilem2  25058  dgrsub2  37705  relexp1idm  38006  relexp0idm  38007