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

Theorem ifbid 3781
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 3780 . 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 1653   ifcif 3763
This theorem is referenced by:  ifbieq2d  3783  ifbieq12d  3785  ifan  3802  ifor  3803  riotabidva  6595  resixpfo  7129  pw2f1olem  7241  unxpdomlem1  7342  cantnflem1d  7673  cantnflem1  7674  dfac12lem1  8054  ttukeylem3  8422  xaddval  10840  xmulcom  10876  xmulneg1  10879  ccatco  11835  sumeq1f  12513  sumsplit  12583  rpnnen2lem1  12845  rpnnen2lem2  12846  rpnnen2lem10  12854  rpnnen  12857  sadadd2lem2  12993  sadfval  12995  sadcp1  12998  sadadd2lem  13002  sadcom  13006  pcmpt  13292  pcmpt2  13293  pcfac  13299  prmrec  13321  ramcl  13428  acsfn  13915  setcepi  14274  frgpup3lem  15440  dpjrid  15651  abvtrivd  15959  psrlidm  16498  psrridm  16499  mvrval  16516  mvrval2  16517  mvrf1  16520  mplmonmul  16558  mplcoe1  16559  mplcoe3  16560  mplcoe2  16561  coe1tm  16696  coe1tmfv2  16698  obsip  16979  fclsval  18071  tmsxpsval2  18600  dscmet  18651  dscopn  18652  ovolicc1  19443  ovolicc  19450  i1f1lem  19610  itg11  19612  i1fpos  19627  itg2uba  19664  itg2split  19670  itg2monolem1  19671  itg2cnlem1  19682  itg2cnlem2  19683  itg2cn  19684  ibllem  19685  isibl  19686  itgeq1f  19692  itgresr  19699  iblpos  19713  itgposval  19716  i1fibl  19728  ibladdlem  19740  iblabslem  19748  itgcn  19763  evlslem3  19966  coe1termlem  20207  coe1term  20208  cxpval  20586  leibpilem2  20812  leibpi  20813  prmorcht  20992  sqff1o  20996  pclogsum  21030  dchr1  21072  dchr2sum  21088  sum2dchr  21089  lgsval  21115  lgsneg  21134  lgsdilem  21137  lgsdir2  21143  lgsdir  21145  dchrisum0flblem2  21234  dchrisum0flb  21235  ostth1  21358  indval  24442  indfval  24445  kur14  24933  prodeq1f  25265  itg2addnclem  26294  itg2gt0cn  26298  ibladdnclem  26299  iblabsnclem  26306  ftc1anclem5  26322  ftc1anc  26326  ftc2nc  26327  pw2f1ocnv  27146  uvcval  27249  uvcvval  27250  flcidc  27394  mamulid  27473  mamurid  27474  refsum2cnlem1  27722  cshwidxmod  28301  sgnval  28616
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 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
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 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3764
  Copyright terms: Public domain W3C validator