Theorem ifbid 3547

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 3546	. 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348  ifcif 3526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-if 3527

This theorem is referenced by:  ifbieq1d  3548  ifbieq2d  3550  ifbieq12d  3552  ifandc  3563  ifordc  3564  nnnninf  7102  nnnninf2  7103  nnnninfeq  7104  nninfisollemne  7107  nninfisol  7109  fodjum  7122  fodju0  7123  fodjuomni  7125  fodjumkv  7136  nninfwlporlemd  7148  nninfwlpor  7150  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  nninfwlpoim  7154  xaddval  9802  0tonninf  10395  1tonninf  10396  sumeq1  11318  summodc  11346  zsumdc  11347  fsum3  11350  isumss  11354  sumsplitdc  11395  prodeq1f  11515  zproddc  11542  fprodseq  11546  pcmpt  12295  pcmpt2  12296  pcfac  12302  lgsval  13699  lgsneg  13719  lgsdilem  13722  lgsdir2  13728  lgsdir  13730  bj-charfunbi  13846  subctctexmid  14034  nninfalllem1  14041  nninfsellemdc  14043  nninfself  14046  nninfsellemeq  14047  nninfsellemqall  14048  nninfsellemeqinf  14049  nninfomni  14052  nninffeq  14053  dceqnconst  14091  dcapnconst  14092