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

Theorem ifid 3599
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 3573 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3574 . 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 1625   ifcif 3567
This theorem is referenced by:  somincom  5082  supsn  7222  wemaplem2  7264  cantnflem1d  7392  cantnflem1  7393  xrmaxeq  10510  xrmineq  10511  xaddpnf1  10555  xaddmnf1  10557  rexmul  10593  max0add  11797  sumz  12197  1arithlem4  12975  xpscf  13470  gsumzsplit  15208  dmdprdsplitlem  15274  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  evlslem2  16251  cnmpt2pc  18428  pcoval2  18516  pcorevlem  18526  itgz  19137  itgvallem3  19142  iblposlem  19148  iblss2  19162  itgss  19168  ditg0  19205  cnplimc  19239  limcco  19245  dvexp3  19327  ply1nzb  19510  plyeq0lem  19594  dgrcolem2  19657  plydivlem4  19678  radcnv0  19794  efrlim  20266  mumullem2  20420  lgsval2lem  20547  lgsdilem2  20572  dgrsub2  27350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-if 3568
  Copyright terms: Public domain W3C validator