Theorem ifbid 3648

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ifcif 3624

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-if 3625

This theorem is referenced by:  ifbieq1d  3649  ifbieq2d  3651  ifbieq12d  3653  ifandc  3667  ifordc  3668  rabsnif  3763  suppsnopdc  6463  pw2f1odclem  7100  2omap  7282  nnnninf  7430  nnnninf2  7431  nnnninfeq  7432  nninfisollemne  7435  nninfisol  7437  fodjum  7450  fodju0  7451  fodjuomni  7453  fodjumkv  7464  nninfwlporlemd  7476  nninfwlpor  7478  nninfwlpoimlemg  7479  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  xaddval  10197  0tonninf  10826  1tonninf  10827  nninfinf  10829  sumeq1  12065  summodc  12094  zsumdc  12095  fsum3  12098  isumss  12102  sumsplitdc  12143  prodeq1f  12263  zproddc  12290  fprodseq  12294  nninfctlemfo  12761  pcmpt  13066  pcmpt2  13067  pcfac  13073  lgsval  16003  lgsneg  16023  lgsdilem  16026  lgsdir2  16032  lgsdir  16034  bj-charfunbi  16707  pw1map  16895  subctctexmid  16900  nninfalllem1  16912  nninfsellemdc  16914  nninfself  16917  nninfsellemeq  16918  nninfsellemqall  16919  nninfsellemeqinf  16920  nninfomni  16923  nninffeq  16924  nnnninfex  16926  dceqnconst  16972  dcapnconst  16973