Theorem ifbid 3570

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ifcif 3549

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-if 3550

This theorem is referenced by:  ifbieq1d  3571  ifbieq2d  3573  ifbieq12d  3575  ifandc  3587  ifordc  3588  pw2f1odclem  6857  nnnninf  7149  nnnninf2  7150  nnnninfeq  7151  nninfisollemne  7154  nninfisol  7156  fodjum  7169  fodju0  7170  fodjuomni  7172  fodjumkv  7183  nninfwlporlemd  7195  nninfwlpor  7197  nninfwlpoimlemg  7198  nninfwlpoimlemginf  7199  nninfwlpoim  7201  xaddval  9870  0tonninf  10465  1tonninf  10466  sumeq1  11390  summodc  11418  zsumdc  11419  fsum3  11422  isumss  11426  sumsplitdc  11467  prodeq1f  11587  zproddc  11614  fprodseq  11618  pcmpt  12370  pcmpt2  12371  pcfac  12377  lgsval  14842  lgsneg  14862  lgsdilem  14865  lgsdir2  14871  lgsdir  14873  bj-charfunbi  15000  subctctexmid  15188  nninfalllem1  15195  nninfsellemdc  15197  nninfself  15200  nninfsellemeq  15201  nninfsellemqall  15202  nninfsellemeqinf  15203  nninfomni  15206  nninffeq  15207  dceqnconst  15246  dcapnconst  15247