Theorem ifbid 3627

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ifcif 3605

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-if 3606

This theorem is referenced by:  ifbieq1d  3628  ifbieq2d  3630  ifbieq12d  3632  ifandc  3646  ifordc  3647  rabsnif  3738  pw2f1odclem  7020  nnnninf  7325  nnnninf2  7326  nnnninfeq  7327  nninfisollemne  7330  nninfisol  7332  fodjum  7345  fodju0  7346  fodjuomni  7348  fodjumkv  7359  nninfwlporlemd  7371  nninfwlpor  7373  nninfwlpoimlemg  7374  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  xaddval  10080  0tonninf  10703  1tonninf  10704  nninfinf  10706  sumeq1  11933  summodc  11962  zsumdc  11963  fsum3  11966  isumss  11970  sumsplitdc  12011  prodeq1f  12131  zproddc  12158  fprodseq  12162  nninfctlemfo  12629  pcmpt  12934  pcmpt2  12935  pcfac  12941  lgsval  15752  lgsneg  15772  lgsdilem  15775  lgsdir2  15781  lgsdir  15783  bj-charfunbi  16457  2omap  16645  pw1map  16647  subctctexmid  16652  nninfalllem1  16661  nninfsellemdc  16663  nninfself  16666  nninfsellemeq  16667  nninfsellemqall  16668  nninfsellemeqinf  16669  nninfomni  16672  nninffeq  16673  nnnninfex  16675  dceqnconst  16716  dcapnconst  16717