MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifid Structured version   Unicode version

Theorem ifid 3976
Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005.)
Assertion
Ref Expression
ifid  |-  if (
ph ,  A ,  A )  =  A

Proof of Theorem ifid
StepHypRef Expression
1 iftrue 3945 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3948 . 2  |-  ( -. 
ph  ->  if ( ph ,  A ,  A )  =  A )
31, 2pm2.61i 164 1  |-  if (
ph ,  A ,  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  csbif  3989  rabsnif  4096  somincom  5404  fsuppmptif  7859  supsn  7930  wemaplem2  7972  cantnflem1d  8107  cantnflem1  8108  cantnflem1dOLD  8130  cantnflem1OLD  8131  xrmaxeq  11380  xrmineq  11381  xaddpnf1  11425  xaddmnf1  11427  rexmul  11463  max0add  13106  sumz  13507  1arithlem4  14303  xpscf  14821  gsumzsplitOLD  16748  dmdprdsplitlem  16886  dmdprdsplitlemOLD  16887  fczpsrbag  17815  mplcoe1  17926  mplcoe3  17927  mplcoe3OLD  17928  mplcoe5  17930  mplcoe2OLD  17932  evlslem2  17979  mdet0  18903  mdetralt2  18906  mdetunilem9  18917  madurid  18941  decpmatid  19066  cnmpt2pc  21191  pcoval2  21279  pcorevlem  21289  itgz  21950  itgvallem3  21955  iblposlem  21961  iblss2  21975  itgss  21981  ditg0  22020  cnplimc  22054  limcco  22060  dvexp3  22142  ply1nzb  22286  plyeq0lem  22370  dgrcolem2  22433  plydivlem4  22454  radcnv0  22573  efrlim  23055  mumullem2  23210  lgsval2lem  23337  lgsdilem2  23362  prod1  28681  dgrsub2  30716
  Copyright terms: Public domain W3C validator