Theorem ifbid 3624

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

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

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 3603

This theorem is referenced by:  ifbieq1d  3625  ifbieq2d  3627  ifbieq12d  3629  ifandc  3643  ifordc  3644  pw2f1odclem  6991  nnnninf  7289  nnnninf2  7290  nnnninfeq  7291  nninfisollemne  7294  nninfisol  7296  fodjum  7309  fodju0  7310  fodjuomni  7312  fodjumkv  7323  nninfwlporlemd  7335  nninfwlpor  7337  nninfwlpoimlemg  7338  nninfwlpoimlemginf  7339  nninfwlpoim  7342  nninfinfwlpo  7343  xaddval  10037  0tonninf  10657  1tonninf  10658  nninfinf  10660  sumeq1  11861  summodc  11889  zsumdc  11890  fsum3  11893  isumss  11897  sumsplitdc  11938  prodeq1f  12058  zproddc  12085  fprodseq  12089  nninfctlemfo  12556  pcmpt  12861  pcmpt2  12862  pcfac  12868  lgsval  15677  lgsneg  15697  lgsdilem  15700  lgsdir2  15706  lgsdir  15708  bj-charfunbi  16132  2omap  16318  pw1map  16320  subctctexmid  16325  nninfalllem1  16333  nninfsellemdc  16335  nninfself  16338  nninfsellemeq  16339  nninfsellemqall  16340  nninfsellemeqinf  16341  nninfomni  16344  nninffeq  16345  nnnninfex  16347  dceqnconst  16387  dcapnconst  16388