Theorem ifbid 3601

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-if 3580

This theorem is referenced by:  ifbieq1d  3602  ifbieq2d  3604  ifbieq12d  3606  ifandc  3620  ifordc  3621  pw2f1odclem  6956  nnnninf  7254  nnnninf2  7255  nnnninfeq  7256  nninfisollemne  7259  nninfisol  7261  fodjum  7274  fodju0  7275  fodjuomni  7277  fodjumkv  7288  nninfwlporlemd  7300  nninfwlpor  7302  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  nninfwlpoim  7307  nninfinfwlpo  7308  xaddval  10002  0tonninf  10622  1tonninf  10623  nninfinf  10625  sumeq1  11781  summodc  11809  zsumdc  11810  fsum3  11813  isumss  11817  sumsplitdc  11858  prodeq1f  11978  zproddc  12005  fprodseq  12009  nninfctlemfo  12476  pcmpt  12781  pcmpt2  12782  pcfac  12788  lgsval  15596  lgsneg  15616  lgsdilem  15619  lgsdir2  15625  lgsdir  15627  bj-charfunbi  15946  2omap  16132  pw1map  16134  subctctexmid  16139  nninfalllem1  16147  nninfsellemdc  16149  nninfself  16152  nninfsellemeq  16153  nninfsellemqall  16154  nninfsellemeqinf  16155  nninfomni  16158  nninffeq  16159  nnnninfex  16161  dceqnconst  16201  dcapnconst  16202