Theorem ifid 4566

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

Syntax hints:   = wceq 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  csbif  4583  rabsnif  4723  somincom  6154  fsuppmptif  9439  supsn  9512  infsn  9545  wemaplem2  9587  cantnflem1  9729  xrmaxeq  13221  xrmineq  13222  xaddpnf1  13268  xaddmnf1  13270  rexmul  13313  max0add  15349  sumz  15758  prod1  15980  1arithlem4  16964  xpscf  17610  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  dmdprdsplitlem  20057  fczpsrbag  21941  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  evlslem2  22103  mdet0  22612  mdetralt2  22615  mdetunilem9  22626  madurid  22650  decpmatid  22776  cnmpopc  24955  pcoval2  25049  pcorevlem  25059  itgz  25816  itgvallem3  25821  iblposlem  25827  iblss2  25841  itgss  25847  ditg0  25888  cnplimc  25922  limcco  25928  dvexp3  26016  ply1nzb  26162  plyeq0lem  26249  dgrcolem2  26314  plydivlem4  26338  radcnv0  26459  efrlim  27012  efrlimOLD  27013  mumullem2  27223  lgsval2lem  27351  lgsdilem2  27377  fsuppind  42600  dgrsub2  43147  sqrtcval  43654  relexp1idm  43727  relexp0idm  43728