Theorem ifbid 3592

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ifcif 3571

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-if 3572

This theorem is referenced by:  ifbieq1d  3593  ifbieq2d  3595  ifbieq12d  3597  ifandc  3610  ifordc  3611  pw2f1odclem  6931  nnnninf  7228  nnnninf2  7229  nnnninfeq  7230  nninfisollemne  7233  nninfisol  7235  fodjum  7248  fodju0  7249  fodjuomni  7251  fodjumkv  7262  nninfwlporlemd  7274  nninfwlpor  7276  nninfwlpoimlemg  7277  nninfwlpoimlemginf  7278  nninfwlpoim  7281  nninfinfwlpo  7282  xaddval  9967  0tonninf  10585  1tonninf  10586  nninfinf  10588  sumeq1  11666  summodc  11694  zsumdc  11695  fsum3  11698  isumss  11702  sumsplitdc  11743  prodeq1f  11863  zproddc  11890  fprodseq  11894  nninfctlemfo  12361  pcmpt  12666  pcmpt2  12667  pcfac  12673  lgsval  15481  lgsneg  15501  lgsdilem  15504  lgsdir2  15510  lgsdir  15512  bj-charfunbi  15747  2omap  15932  subctctexmid  15937  nninfalllem1  15945  nninfsellemdc  15947  nninfself  15950  nninfsellemeq  15951  nninfsellemqall  15952  nninfsellemeqinf  15953  nninfomni  15956  nninffeq  15957  nnnninfex  15959  dceqnconst  15999  dcapnconst  16000