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

Theorem ifid 3771
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 3745 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3746 . 2  |-  ( -. 
ph  ->  if ( ph ,  A ,  A )  =  A )
31, 2pm2.61i 158 1  |-  if (
ph ,  A ,  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652   ifcif 3739
This theorem is referenced by:  somincom  5271  supsn  7474  wemaplem2  7516  cantnflem1d  7644  cantnflem1  7645  xrmaxeq  10767  xrmineq  10768  xaddpnf1  10812  xaddmnf1  10814  rexmul  10850  max0add  12115  sumz  12516  1arithlem4  13294  xpscf  13791  gsumzsplit  15529  dmdprdsplitlem  15595  mplcoe1  16528  mplcoe3  16529  mplcoe2  16530  evlslem2  16568  cnmpt2pc  18953  pcoval2  19041  pcorevlem  19051  itgz  19672  itgvallem3  19677  iblposlem  19683  iblss2  19697  itgss  19703  ditg0  19740  cnplimc  19774  limcco  19780  dvexp3  19862  ply1nzb  20045  plyeq0lem  20129  dgrcolem2  20192  plydivlem4  20213  radcnv0  20332  efrlim  20808  mumullem2  20963  lgsval2lem  21090  lgsdilem2  21115  prod1  25270  dgrsub2  27316
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-if 3740
  Copyright terms: Public domain W3C validator