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

Theorem ifid 3598
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 3572 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3573 . 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 3566
This theorem is referenced by:  somincom  5079  supsn  7216  wemaplem2  7258  cantnflem1d  7386  cantnflem1  7387  xrmaxeq  10504  xrmineq  10505  xaddpnf1  10549  xaddmnf1  10551  rexmul  10587  max0add  11791  sumz  12191  1arithlem4  12969  xpscf  13464  gsumzsplit  15202  dmdprdsplitlem  15268  mplcoe1  16205  mplcoe3  16206  mplcoe2  16207  evlslem2  16245  cnmpt2pc  18422  pcoval2  18510  pcorevlem  18520  itgz  19131  itgvallem3  19136  iblposlem  19142  iblss2  19156  itgss  19162  ditg0  19199  cnplimc  19233  limcco  19239  dvexp3  19321  ply1nzb  19504  plyeq0lem  19588  dgrcolem2  19651  plydivlem4  19672  radcnv0  19788  efrlim  20260  mumullem2  20414  lgsval2lem  20541  lgsdilem2  20566  dgrsub2  26750
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-if 3567
  Copyright terms: Public domain W3C validator