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

Theorem ifbid 3659
Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
Hypothesis
Ref Expression
ifbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ifbid  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)

Proof of Theorem ifbid
StepHypRef Expression
1 ifbid.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 ifbi 3658 . 2  |-  ( ( ps  <->  ch )  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B ) )
31, 2syl 15 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642   ifcif 3641
This theorem is referenced by:  ifbieq2d  3661  ifbieq12d  3663  ifan  3680  ifor  3681  riotabidva  6405  resixpfo  6939  pw2f1olem  7051  unxpdomlem1  7152  cantnflem1d  7477  cantnflem1  7478  dfac12lem1  7856  ttukeylem3  8225  xaddval  10639  xmulcom  10675  xmulneg1  10678  ccatco  11580  sumeq1f  12252  sumsplit  12322  rpnnen2lem1  12584  rpnnen2lem2  12585  rpnnen2lem10  12593  rpnnen  12596  sadadd2lem2  12732  sadfval  12734  sadcp1  12737  sadadd2lem  12741  sadcom  12745  pcmpt  13031  pcmpt2  13032  pcfac  13038  prmrec  13060  ramcl  13167  acsfn  13654  setcepi  14013  frgpup3lem  15179  dpjrid  15390  abvtrivd  15698  psrlidm  16241  psrridm  16242  mvrval  16259  mvrval2  16260  mvrf1  16263  mplmonmul  16301  mplcoe1  16302  mplcoe3  16303  mplcoe2  16304  coe1tm  16442  coe1tmfv2  16444  obsip  16721  fclsval  17799  tmsxpsval2  18181  dscmet  18191  dscopn  18192  ovolicc1  18973  ovolicc  18980  i1f1lem  19142  itg11  19144  i1fpos  19159  itg2uba  19196  itg2split  19202  itg2monolem1  19203  itg2cnlem1  19214  itg2cnlem2  19215  itg2cn  19216  ibllem  19217  isibl  19218  itgeq1f  19224  itgresr  19231  iblpos  19245  itgposval  19248  i1fibl  19260  ibladdlem  19272  iblabslem  19280  itgcn  19295  evlslem3  19496  coe1termlem  19737  coe1term  19738  cxpval  20116  leibpilem2  20342  leibpi  20343  prmorcht  20522  sqff1o  20526  pclogsum  20560  dchr1  20602  dchr2sum  20618  sum2dchr  20619  lgsval  20645  lgsneg  20664  lgsdilem  20667  lgsdir2  20673  lgsdir  20675  dchrisum0flblem2  20764  dchrisum0flb  20765  ostth1  20888  indval  23677  indfval  23680  kur14  24151  prodeq1f  24535  itg2addnclem  25492  itg2gt0cn  25495  ibladdnclem  25496  iblabsnclem  25503  pw2f1ocnv  26453  uvcval  26557  uvcvval  26558  flcidc  26702  mamulid  26781  mamurid  26782  refsum2cnlem1  27031  sgnval  27928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-if 3642
  Copyright terms: Public domain W3C validator