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

Theorem ifbid 3583
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 3582 . 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 1623   ifcif 3565
This theorem is referenced by:  ifbieq2d  3585  ifbieq12d  3587  ifan  3604  ifor  3605  riotabidva  6321  resixpfo  6854  pw2f1olem  6966  unxpdomlem1  7067  cantnflem1d  7390  cantnflem1  7391  dfac12lem1  7769  ttukeylem3  8138  xaddval  10550  xmulcom  10586  xmulneg1  10589  ccatco  11490  sumeq1f  12161  sumsplit  12231  rpnnen2lem1  12493  rpnnen2lem2  12494  rpnnen2lem10  12502  rpnnen  12505  sadadd2lem2  12641  sadfval  12643  sadcp1  12646  sadadd2lem  12650  sadcom  12654  pcmpt  12940  pcmpt2  12941  pcfac  12947  prmrec  12969  ramcl  13076  acsfn  13561  setcepi  13920  frgpup3lem  15086  dpjrid  15297  abvtrivd  15605  psrlidm  16148  psrridm  16149  mvrval  16166  mvrval2  16167  mvrf1  16170  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  coe1tm  16349  coe1tmfv2  16351  obsip  16621  fclsval  17703  tmsxpsval2  18085  dscmet  18095  dscopn  18096  ovolicc1  18875  ovolicc  18882  i1f1lem  19044  itg11  19046  i1fpos  19061  itg2uba  19098  itg2split  19104  itg2monolem1  19105  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  ibllem  19119  isibl  19120  itgeq1f  19126  itgresr  19133  iblpos  19147  itgposval  19150  i1fibl  19162  ibladdlem  19174  iblabslem  19182  itgcn  19197  evlslem3  19398  coe1termlem  19639  coe1term  19640  cxpval  20011  leibpilem2  20237  leibpi  20238  prmorcht  20416  sqff1o  20420  pclogsum  20454  dchr1  20496  dchr2sum  20512  sum2dchr  20513  lgsval  20539  lgsneg  20558  lgsdilem  20561  lgsdir2  20567  lgsdir  20569  dchrisum0flblem2  20658  dchrisum0flb  20659  ostth1  20782  indval  23597  indfval  23600  kur14  23747  repcpwti  25161  pw2f1ocnv  27130  uvcval  27234  uvcvval  27235  flcidc  27379  mamulid  27458  mamurid  27459  refsum2cnlem1  27708  sgnval  28245
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator