Theorem ifbieq1d 3628

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq1d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 3627	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 3623	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2264	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-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  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-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804  df-un 3204  df-if 3606

This theorem is referenced by:  ctssdclemn0  7309  ctssdc  7312  enumctlemm  7313  iseqf1olemfvp  10773  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  bcval  11012  swrdval  11233  sumrbdclem  11943  summodclem3  11946  summodclem2a  11947  summodc  11949  zsumdc  11950  fsum3  11953  isumss  11957  isumss2  11959  fsum3cvg2  11960  fsum3ser  11963  fsumcl2lem  11964  fsumadd  11972  sumsnf  11975  fsummulc2  12014  isumlessdc  12062  cbvprod  12124  prodrbdclem  12137  prodmodclem3  12141  prodmodclem2a  12142  prodmodc  12144  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prodssdc  12155  fprodmul  12157  prodsnf  12158  pcmpt  12921  pcmptdvds  12923  elply2  15465  lgsval  15739  lgsfvalg  15740  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773