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

Theorem ifid 3686
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 3660 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3661 . 2  |-  ( -. 
ph  ->  if ( ph ,  A ,  A )  =  A )
31, 2pm2.61i 156 1  |-  if (
ph ,  A ,  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1647   ifcif 3654
This theorem is referenced by:  somincom  5183  supsn  7367  wemaplem2  7409  cantnflem1d  7537  cantnflem1  7538  xrmaxeq  10660  xrmineq  10661  xaddpnf1  10705  xaddmnf1  10707  rexmul  10743  max0add  12002  sumz  12403  1arithlem4  13181  xpscf  13678  gsumzsplit  15416  dmdprdsplitlem  15482  mplcoe1  16419  mplcoe3  16420  mplcoe2  16421  evlslem2  16459  cnmpt2pc  18641  pcoval2  18729  pcorevlem  18739  itgz  19350  itgvallem3  19355  iblposlem  19361  iblss2  19375  itgss  19381  ditg0  19418  cnplimc  19452  limcco  19458  dvexp3  19540  ply1nzb  19723  plyeq0lem  19807  dgrcolem2  19870  plydivlem4  19891  radcnv0  20010  efrlim  20486  mumullem2  20641  lgsval2lem  20768  lgsdilem2  20793  prod1  24839  dgrsub2  26930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-if 3655
  Copyright terms: Public domain W3C validator