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

Theorem ifbid 3785
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 3784 . 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 178    = wceq 1654   ifcif 3767
This theorem is referenced by:  ifbieq2d  3787  ifbieq12d  3789  ifan  3805  ifor  3806  riotabidva  6602  resixpfo  7136  pw2f1olem  7248  unxpdomlem1  7349  cantnflem1d  7680  cantnflem1  7681  dfac12lem1  8061  ttukeylem3  8429  xaddval  10847  xmulcom  10883  xmulneg1  10886  ccatco  11842  sumeq1f  12520  sumsplit  12590  rpnnen2lem1  12852  rpnnen2lem2  12853  rpnnen2lem10  12861  rpnnen  12864  sadadd2lem2  13000  sadfval  13002  sadcp1  13005  sadadd2lem  13009  sadcom  13013  pcmpt  13299  pcmpt2  13300  pcfac  13306  prmrec  13328  ramcl  13435  acsfn  13922  setcepi  14281  frgpup3lem  15447  dpjrid  15658  abvtrivd  15966  psrlidm  16505  psrridm  16506  mvrval  16523  mvrval2  16524  mvrf1  16527  mplmonmul  16565  mplcoe1  16566  mplcoe3  16567  mplcoe2  16568  coe1tm  16703  coe1tmfv2  16705  obsip  16986  fclsval  18078  tmsxpsval2  18607  dscmet  18658  dscopn  18659  ovolicc1  19450  ovolicc  19457  i1f1lem  19617  itg11  19619  i1fpos  19634  itg2uba  19671  itg2split  19677  itg2monolem1  19678  itg2cnlem1  19689  itg2cnlem2  19690  itg2cn  19691  ibllem  19692  isibl  19693  itgeq1f  19699  itgresr  19706  iblpos  19720  itgposval  19723  i1fibl  19735  ibladdlem  19747  iblabslem  19755  itgcn  19770  evlslem3  19973  coe1termlem  20214  coe1term  20215  cxpval  20593  leibpilem2  20819  leibpi  20820  prmorcht  20999  sqff1o  21003  pclogsum  21037  dchr1  21079  dchr2sum  21095  sum2dchr  21096  lgsval  21122  lgsneg  21141  lgsdilem  21144  lgsdir2  21150  lgsdir  21152  dchrisum0flblem2  21241  dchrisum0flb  21242  ostth1  21365  indval  24446  indfval  24449  kur14  24937  prodeq1f  25269  itg2addnclem  26298  itg2gt0cn  26302  ibladdnclem  26303  iblabsnclem  26310  ftc1anclem5  26326  ftc1anc  26330  ftc2nc  26331  pw2f1ocnv  27220  uvcval  27323  uvcvval  27324  flcidc  27468  mamulid  27547  mamurid  27548  refsum2cnlem1  27796  cshwidxmod  28375  sgnval  28690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3768
  Copyright terms: Public domain W3C validator