Theorem ifbid 3591

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)

Hypothesis

Ref	Expression
ifbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ifbid	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Proof of Theorem ifbid

Step	Hyp	Ref	Expression
1		ifbid.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		ifbi 3590	. 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372  ifcif 3570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-if 3571

This theorem is referenced by:  ifbieq1d  3592  ifbieq2d  3594  ifbieq12d  3596  ifandc  3609  ifordc  3610  pw2f1odclem  6930  nnnninf  7227  nnnninf2  7228  nnnninfeq  7229  nninfisollemne  7232  nninfisol  7234  fodjum  7247  fodju0  7248  fodjuomni  7250  fodjumkv  7261  nninfwlporlemd  7273  nninfwlpor  7275  nninfwlpoimlemg  7276  nninfwlpoimlemginf  7277  nninfwlpoim  7280  nninfinfwlpo  7281  xaddval  9966  0tonninf  10583  1tonninf  10584  nninfinf  10586  sumeq1  11637  summodc  11665  zsumdc  11666  fsum3  11669  isumss  11673  sumsplitdc  11714  prodeq1f  11834  zproddc  11861  fprodseq  11865  nninfctlemfo  12332  pcmpt  12637  pcmpt2  12638  pcfac  12644  lgsval  15452  lgsneg  15472  lgsdilem  15475  lgsdir2  15481  lgsdir  15483  bj-charfunbi  15709  2omap  15894  subctctexmid  15899  nninfalllem1  15907  nninfsellemdc  15909  nninfself  15912  nninfsellemeq  15913  nninfsellemqall  15914  nninfsellemeqinf  15915  nninfomni  15918  nninffeq  15919  nnnninfex  15921  dceqnconst  15961  dcapnconst  15962