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

Theorem ifid 3826
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 3797 . 2  |-  ( ph  ->  if ( ph ,  A ,  A )  =  A )
2 iffalse 3799 . 2  |-  ( -. 
ph  ->  if ( ph ,  A ,  A )  =  A )
31, 2pm2.61i 164 1  |-  if (
ph ,  A ,  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   ifcif 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3792
This theorem is referenced by:  csbif  3839  rabsnif  3944  somincom  5235  fsuppmptif  7649  supsn  7719  wemaplem2  7761  cantnflem1d  7896  cantnflem1  7897  cantnflem1dOLD  7919  cantnflem1OLD  7920  xrmaxeq  11151  xrmineq  11152  xaddpnf1  11196  xaddmnf1  11198  rexmul  11234  max0add  12799  sumz  13199  1arithlem4  13987  xpscf  14504  gsumzsplitOLD  16419  dmdprdsplitlem  16534  dmdprdsplitlemOLD  16535  fczpsrbag  17434  mplcoe1  17544  mplcoe3  17545  mplcoe3OLD  17546  mplcoe5  17548  mplcoe2OLD  17550  evlslem2  17597  mdetralt2  18415  mdetunilem9  18426  madurid  18450  cnmpt2pc  20500  pcoval2  20588  pcorevlem  20598  itgz  21258  itgvallem3  21263  iblposlem  21269  iblss2  21283  itgss  21289  ditg0  21328  cnplimc  21362  limcco  21368  dvexp3  21450  ply1nzb  21594  plyeq0lem  21678  dgrcolem2  21741  plydivlem4  21762  radcnv0  21881  efrlim  22363  mumullem2  22518  lgsval2lem  22645  lgsdilem2  22670  prod1  27457  dgrsub2  29491  pmatcollpw1id  30899  mdet0  30933
  Copyright terms: Public domain W3C validator