Theorem ifbid 3625

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ifcif 3603

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-if 3604

This theorem is referenced by:  ifbieq1d  3626  ifbieq2d  3628  ifbieq12d  3630  ifandc  3644  ifordc  3645  rabsnif  3736  pw2f1odclem  7015  nnnninf  7316  nnnninf2  7317  nnnninfeq  7318  nninfisollemne  7321  nninfisol  7323  fodjum  7336  fodju0  7337  fodjuomni  7339  fodjumkv  7350  nninfwlporlemd  7362  nninfwlpor  7364  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  nninfwlpoim  7369  nninfinfwlpo  7370  xaddval  10070  0tonninf  10692  1tonninf  10693  nninfinf  10695  sumeq1  11906  summodc  11934  zsumdc  11935  fsum3  11938  isumss  11942  sumsplitdc  11983  prodeq1f  12103  zproddc  12130  fprodseq  12134  nninfctlemfo  12601  pcmpt  12906  pcmpt2  12907  pcfac  12913  lgsval  15723  lgsneg  15743  lgsdilem  15746  lgsdir2  15752  lgsdir  15754  bj-charfunbi  16342  2omap  16530  pw1map  16532  subctctexmid  16537  nninfalllem1  16546  nninfsellemdc  16548  nninfself  16551  nninfsellemeq  16552  nninfsellemqall  16553  nninfsellemeqinf  16554  nninfomni  16557  nninffeq  16558  nnnninfex  16560  dceqnconst  16600  dcapnconst  16601