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

Theorem ifid 3597
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 3571 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3572 . 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 1623   ifcif 3565
This theorem is referenced by:  somincom  5080  supsn  7220  wemaplem2  7262  cantnflem1d  7390  cantnflem1  7391  xrmaxeq  10508  xrmineq  10509  xaddpnf1  10553  xaddmnf1  10555  rexmul  10591  max0add  11795  sumz  12195  1arithlem4  12973  xpscf  13468  gsumzsplit  15206  dmdprdsplitlem  15272  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  evlslem2  16249  cnmpt2pc  18426  pcoval2  18514  pcorevlem  18524  itgz  19135  itgvallem3  19140  iblposlem  19146  iblss2  19160  itgss  19166  ditg0  19203  cnplimc  19237  limcco  19243  dvexp3  19325  ply1nzb  19508  plyeq0lem  19592  dgrcolem2  19655  plydivlem4  19676  radcnv0  19792  efrlim  20264  mumullem2  20418  lgsval2lem  20545  lgsdilem2  20570  dgrsub2  27339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator