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

Theorem ifid 3763
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 3737 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3738 . 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 3731
This theorem is referenced by:  somincom  5263  supsn  7466  wemaplem2  7508  cantnflem1d  7636  cantnflem1  7637  xrmaxeq  10759  xrmineq  10760  xaddpnf1  10804  xaddmnf1  10806  rexmul  10842  max0add  12107  sumz  12508  1arithlem4  13286  xpscf  13783  gsumzsplit  15521  dmdprdsplitlem  15587  mplcoe1  16520  mplcoe3  16521  mplcoe2  16522  evlslem2  16560  cnmpt2pc  18945  pcoval2  19033  pcorevlem  19043  itgz  19664  itgvallem3  19669  iblposlem  19675  iblss2  19689  itgss  19695  ditg0  19732  cnplimc  19766  limcco  19772  dvexp3  19854  ply1nzb  20037  plyeq0lem  20121  dgrcolem2  20184  plydivlem4  20205  radcnv0  20324  efrlim  20800  mumullem2  20955  lgsval2lem  21082  lgsdilem2  21107  prod1  25262  dgrsub2  27307
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator