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

Theorem ifid 3963
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 3932 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3935 . 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 1383   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927
This theorem is referenced by:  csbif  3976  rabsnif  4084  somincom  5394  fsuppmptif  7861  supsn  7933  wemaplem2  7975  cantnflem1  8111  cantnflem1dOLD  8133  cantnflem1OLD  8134  xrmaxeq  11391  xrmineq  11392  xaddpnf1  11436  xaddmnf1  11438  rexmul  11474  max0add  13125  sumz  13526  prod1  13733  1arithlem4  14426  xpscf  14945  mgm2nsgrplem2  16016  mgm2nsgrplem3  16017  gsumzsplitOLD  16924  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  fczpsrbag  17995  mplcoe1  18106  mplcoe3  18107  mplcoe3OLD  18108  mplcoe5  18110  mplcoe2OLD  18112  evlslem2  18159  mdet0  19086  mdetralt2  19089  mdetunilem9  19100  madurid  19124  decpmatid  19249  cnmpt2pc  21406  pcoval2  21494  pcorevlem  21504  itgz  22165  itgvallem3  22170  iblposlem  22176  iblss2  22190  itgss  22196  ditg0  22235  cnplimc  22269  limcco  22275  dvexp3  22357  ply1nzb  22501  plyeq0lem  22585  dgrcolem2  22649  plydivlem4  22670  radcnv0  22789  efrlim  23277  mumullem2  23432  lgsval2lem  23559  lgsdilem2  23584  dgrsub2  31060
  Copyright terms: Public domain W3C validator