Theorem ifbid 3659

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402  ifcif 3635

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-if 3636

This theorem is referenced by:  ifbieq1d  3660  ifbieq2d  3662  ifbieq12d  3664  ifandc  3678  ifordc  3679  rabsnif  3774  suppsnopdc  6480  pw2f1odclem  7124  2omap  7308  nnnninf  7456  nnnninf2  7457  nnnninfeq  7458  nninfisollemne  7461  nninfisol  7463  fodjum  7476  fodju0  7477  fodjuomni  7479  fodjumkv  7490  nninfwlporlemd  7502  nninfwlpor  7504  nninfwlpoimlemg  7505  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  xaddval  10226  0tonninf  10855  1tonninf  10856  nninfinf  10858  sumeq1  12099  summodc  12128  zsumdc  12129  fsum3  12132  isumss  12136  sumsplitdc  12177  prodeq1f  12297  zproddc  12324  fprodseq  12328  nninfctlemfo  12795  pcmpt  13100  pcmpt2  13101  pcfac  13107  lgsval  16037  lgsneg  16057  lgsdilem  16060  lgsdir2  16066  lgsdir  16068  bj-charfunbi  16751  pw1map  16939  subctctexmid  16944  nninfalllem1  16956  nninfsellemdc  16958  nninfself  16961  nninfsellemeq  16962  nninfsellemqall  16963  nninfsellemeqinf  16964  nninfomni  16967  nninffeq  16968  nnnninfex  16970  dceqnconst  17015  dcapnconst  17016