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  10772  seq3f1olemqsum  10775  seq3f1oleml  10778  seq3f1o  10779  bcval  11011  swrdval  11229  sumrbdclem  11939  summodclem3  11942  summodclem2a  11943  summodc  11945  zsumdc  11946  fsum3  11949  isumss  11953  isumss2  11955  fsum3cvg2  11956  fsum3ser  11959  fsumcl2lem  11960  fsumadd  11968  sumsnf  11971  fsummulc2  12010  isumlessdc  12058  cbvprod  12120  prodrbdclem  12133  prodmodclem3  12137  prodmodclem2a  12138  prodmodc  12140  zproddc  12141  fprodseq  12145  fprodntrivap  12146  prodssdc  12151  fprodmul  12153  prodsnf  12154  pcmpt  12917  pcmptdvds  12919  elply2  15461  lgsval  15735  lgsfvalg  15736  lgsdir  15766  lgsdilem2  15767  lgsdi  15768  lgsne0  15769