Theorem ifbid 3644

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-if 3621

This theorem is referenced by:  ifbieq1d  3645  ifbieq2d  3647  ifbieq12d  3649  ifandc  3663  ifordc  3664  rabsnif  3758  suppsnopdc  6450  pw2f1odclem  7087  2omap  7269  nnnninf  7417  nnnninf2  7418  nnnninfeq  7419  nninfisollemne  7422  nninfisol  7424  fodjum  7437  fodju0  7438  fodjuomni  7440  fodjumkv  7451  nninfwlporlemd  7463  nninfwlpor  7465  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  nninfwlpoim  7470  nninfinfwlpo  7471  xaddval  10178  0tonninf  10802  1tonninf  10803  nninfinf  10805  sumeq1  12040  summodc  12069  zsumdc  12070  fsum3  12073  isumss  12077  sumsplitdc  12118  prodeq1f  12238  zproddc  12265  fprodseq  12269  nninfctlemfo  12736  pcmpt  13041  pcmpt2  13042  pcfac  13048  lgsval  15877  lgsneg  15897  lgsdilem  15900  lgsdir2  15906  lgsdir  15908  bj-charfunbi  16581  pw1map  16769  subctctexmid  16774  nninfalllem1  16786  nninfsellemdc  16788  nninfself  16791  nninfsellemeq  16792  nninfsellemqall  16793  nninfsellemeqinf  16794  nninfomni  16797  nninffeq  16798  nnnninfex  16800  dceqnconst  16846  dcapnconst  16847