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

Theorem ifbid 3725
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 3724 . 2  |-  ( ( ps  <->  ch )  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B ) )
31, 2syl 16 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   ifcif 3707
This theorem is referenced by:  ifbieq2d  3727  ifbieq12d  3729  ifan  3746  ifor  3747  riotabidva  6533  resixpfo  7067  pw2f1olem  7179  unxpdomlem1  7280  cantnflem1d  7608  cantnflem1  7609  dfac12lem1  7987  ttukeylem3  8355  xaddval  10773  xmulcom  10809  xmulneg1  10812  ccatco  11767  sumeq1f  12445  sumsplit  12515  rpnnen2lem1  12777  rpnnen2lem2  12778  rpnnen2lem10  12786  rpnnen  12789  sadadd2lem2  12925  sadfval  12927  sadcp1  12930  sadadd2lem  12934  sadcom  12938  pcmpt  13224  pcmpt2  13225  pcfac  13231  prmrec  13253  ramcl  13360  acsfn  13847  setcepi  14206  frgpup3lem  15372  dpjrid  15583  abvtrivd  15891  psrlidm  16430  psrridm  16431  mvrval  16448  mvrval2  16449  mvrf1  16452  mplmonmul  16490  mplcoe1  16491  mplcoe3  16492  mplcoe2  16493  coe1tm  16628  coe1tmfv2  16630  obsip  16911  fclsval  18001  tmsxpsval2  18530  dscmet  18581  dscopn  18582  ovolicc1  19373  ovolicc  19380  i1f1lem  19542  itg11  19544  i1fpos  19559  itg2uba  19596  itg2split  19602  itg2monolem1  19603  itg2cnlem1  19614  itg2cnlem2  19615  itg2cn  19616  ibllem  19617  isibl  19618  itgeq1f  19624  itgresr  19631  iblpos  19645  itgposval  19648  i1fibl  19660  ibladdlem  19672  iblabslem  19680  itgcn  19695  evlslem3  19896  coe1termlem  20137  coe1term  20138  cxpval  20516  leibpilem2  20742  leibpi  20743  prmorcht  20922  sqff1o  20926  pclogsum  20960  dchr1  21002  dchr2sum  21018  sum2dchr  21019  lgsval  21045  lgsneg  21064  lgsdilem  21067  lgsdir2  21073  lgsdir  21075  dchrisum0flblem2  21164  dchrisum0flb  21165  ostth1  21288  indval  24372  indfval  24375  kur14  24863  prodeq1f  25195  itg2addnclem  26163  itg2gt0cn  26167  ibladdnclem  26168  iblabsnclem  26175  pw2f1ocnv  27006  uvcval  27110  uvcvval  27111  flcidc  27255  mamulid  27334  mamurid  27335  refsum2cnlem1  27583  sgnval  28240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-if 3708
  Copyright terms: Public domain W3C validator