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  7003  nnnninf  7304  nnnninf2  7305  nnnninfeq  7306  nninfisollemne  7309  nninfisol  7311  fodjum  7324  fodju0  7325  fodjuomni  7327  fodjumkv  7338  nninfwlporlemd  7350  nninfwlpor  7352  nninfwlpoimlemg  7353  nninfwlpoimlemginf  7354  nninfwlpoim  7357  nninfinfwlpo  7358  xaddval  10053  0tonninf  10674  1tonninf  10675  nninfinf  10677  sumeq1  11881  summodc  11909  zsumdc  11910  fsum3  11913  isumss  11917  sumsplitdc  11958  prodeq1f  12078  zproddc  12105  fprodseq  12109  nninfctlemfo  12576  pcmpt  12881  pcmpt2  12882  pcfac  12888  lgsval  15698  lgsneg  15718  lgsdilem  15721  lgsdir2  15727  lgsdir  15729  bj-charfunbi  16229  2omap  16418  pw1map  16420  subctctexmid  16425  nninfalllem1  16434  nninfsellemdc  16436  nninfself  16439  nninfsellemeq  16440  nninfsellemqall  16441  nninfsellemeqinf  16442  nninfomni  16445  nninffeq  16446  nnnninfex  16448  dceqnconst  16488  dcapnconst  16489