Theorem ifbieq1d 3554

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 3553	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 3549	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2208	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ifcif 3532

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737  df-un 3131  df-if 3533

This theorem is referenced by:  ctssdclemn0  7099  ctssdc  7102  enumctlemm  7103  iseqf1olemfvp  10465  seq3f1olemqsum  10468  seq3f1oleml  10471  seq3f1o  10472  bcval  10695  sumrbdclem  11351  summodclem3  11354  summodclem2a  11355  summodc  11357  zsumdc  11358  fsum3  11361  isumss  11365  isumss2  11367  fsum3cvg2  11368  fsum3ser  11371  fsumcl2lem  11372  fsumadd  11380  sumsnf  11383  fsummulc2  11422  isumlessdc  11470  cbvprod  11532  prodrbdclem  11545  prodmodclem3  11549  prodmodclem2a  11550  prodmodc  11552  zproddc  11553  fprodseq  11557  fprodntrivap  11558  prodssdc  11563  fprodmul  11565  prodsnf  11566  pcmpt  12306  pcmptdvds  12308  lgsval  13956  lgsfvalg  13957  lgsdir  13987  lgsdilem2  13988  lgsdi  13989  lgsne0  13990