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

Theorem ifid 3823
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 3794 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3796 . 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 1364   ifcif 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-if 3789
This theorem is referenced by:  csbif  3836  rabsnif  3941  somincom  5232  fsuppmptif  7645  supsn  7715  wemaplem2  7757  cantnflem1d  7892  cantnflem1  7893  cantnflem1dOLD  7915  cantnflem1OLD  7916  xrmaxeq  11147  xrmineq  11148  xaddpnf1  11192  xaddmnf1  11194  rexmul  11230  max0add  12795  sumz  13195  1arithlem4  13983  xpscf  14500  gsumzsplitOLD  16412  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  fczpsrbag  17424  mplcoe1  17534  mplcoe3  17535  mplcoe3OLD  17536  mplcoe2  17537  mplcoe2OLD  17538  evlslem2  17581  mdetralt2  18315  mdetunilem9  18326  madurid  18350  cnmpt2pc  20400  pcoval2  20488  pcorevlem  20498  itgz  21158  itgvallem3  21163  iblposlem  21169  iblss2  21183  itgss  21189  ditg0  21228  cnplimc  21262  limcco  21268  dvexp3  21350  ply1nzb  21537  plyeq0lem  21621  dgrcolem2  21684  plydivlem4  21705  radcnv0  21824  efrlim  22306  mumullem2  22461  lgsval2lem  22588  lgsdilem2  22613  prod1  27370  dgrsub2  29400  mdet0  30757
  Copyright terms: Public domain W3C validator