Theorem ifid 3978

Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)

Assertion

Ref	Expression
ifid

Proof of Theorem ifid

Step	Hyp	Ref	Expression
1		iftrue 3947	. 2
2		iffalse 3950	. 2
3	1, 2	pm2.61i 164	1

Syntax hints:  =wceq 1395  ifcif 3941

This theorem is referenced by:  csbif  3991  rabsnif  4099  somincom  5409  fsuppmptif  7879  supsn  7951  wemaplem2  7993  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  xrmaxeq  11409  xrmineq  11410  xaddpnf1  11454  xaddmnf1  11456  rexmul  11492  max0add  13143  sumz  13544  prod1  13751  1arithlem4  14444  xpscf  14963  mgm2nsgrplem2  16037  mgm2nsgrplem3  16038  gsumzsplitOLD  16945  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  fczpsrbag  18016  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  evlslem2  18180  mdet0  19108  mdetralt2  19111  mdetunilem9  19122  madurid  19146  decpmatid  19271  cnmpt2pc  21428  pcoval2  21516  pcorevlem  21526  itgz  22187  itgvallem3  22192  iblposlem  22198  iblss2  22212  itgss  22218  ditg0  22257  cnplimc  22291  limcco  22297  dvexp3  22379  ply1nzb  22523  plyeq0lem  22607  dgrcolem2  22671  plydivlem4  22692  radcnv0  22811  efrlim  23299  mumullem2  23454  lgsval2lem  23581  lgsdilem2  23606  dgrsub2  31084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942