Theorem ifbid 3627

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ifcif 3605

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-if 3606

This theorem is referenced by:  ifbieq1d  3628  ifbieq2d  3630  ifbieq12d  3632  ifandc  3646  ifordc  3647  rabsnif  3738  pw2f1odclem  7019  nnnninf  7324  nnnninf2  7325  nnnninfeq  7326  nninfisollemne  7329  nninfisol  7331  fodjum  7344  fodju0  7345  fodjuomni  7347  fodjumkv  7358  nninfwlporlemd  7370  nninfwlpor  7372  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  xaddval  10079  0tonninf  10701  1tonninf  10702  nninfinf  10704  sumeq1  11915  summodc  11943  zsumdc  11944  fsum3  11947  isumss  11951  sumsplitdc  11992  prodeq1f  12112  zproddc  12139  fprodseq  12143  nninfctlemfo  12610  pcmpt  12915  pcmpt2  12916  pcfac  12922  lgsval  15732  lgsneg  15752  lgsdilem  15755  lgsdir2  15761  lgsdir  15763  bj-charfunbi  16406  2omap  16594  pw1map  16596  subctctexmid  16601  nninfalllem1  16610  nninfsellemdc  16612  nninfself  16615  nninfsellemeq  16616  nninfsellemqall  16617  nninfsellemeqinf  16618  nninfomni  16621  nninffeq  16622  nnnninfex  16624  dceqnconst  16664  dcapnconst  16665