Theorem ifbid 3631

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ifcif 3607

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-if 3608

This theorem is referenced by:  ifbieq1d  3632  ifbieq2d  3634  ifbieq12d  3636  ifandc  3650  ifordc  3651  rabsnif  3742  suppsnopdc  6428  pw2f1odclem  7063  nnnninf  7368  nnnninf2  7369  nnnninfeq  7370  nninfisollemne  7373  nninfisol  7375  fodjum  7388  fodju0  7389  fodjuomni  7391  fodjumkv  7402  nninfwlporlemd  7414  nninfwlpor  7416  nninfwlpoimlemg  7417  nninfwlpoimlemginf  7418  nninfwlpoim  7421  nninfinfwlpo  7422  xaddval  10124  0tonninf  10748  1tonninf  10749  nninfinf  10751  sumeq1  11978  summodc  12007  zsumdc  12008  fsum3  12011  isumss  12015  sumsplitdc  12056  prodeq1f  12176  zproddc  12203  fprodseq  12207  nninfctlemfo  12674  pcmpt  12979  pcmpt2  12980  pcfac  12986  lgsval  15806  lgsneg  15826  lgsdilem  15829  lgsdir2  15835  lgsdir  15837  bj-charfunbi  16510  2omap  16698  pw1map  16700  subctctexmid  16705  nninfalllem1  16717  nninfsellemdc  16719  nninfself  16722  nninfsellemeq  16723  nninfsellemqall  16724  nninfsellemeqinf  16725  nninfomni  16728  nninffeq  16729  nnnninfex  16731  dceqnconst  16776  dcapnconst  16777