Theorem ifbieq1d 3568

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1363  ifcif 3546

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rab 2474  df-v 2751  df-un 3145  df-if 3547

This theorem is referenced by:  ctssdclemn0  7122  ctssdc  7125  enumctlemm  7126  iseqf1olemfvp  10510  seq3f1olemqsum  10513  seq3f1oleml  10516  seq3f1o  10517  bcval  10742  sumrbdclem  11398  summodclem3  11401  summodclem2a  11402  summodc  11404  zsumdc  11405  fsum3  11408  isumss  11412  isumss2  11414  fsum3cvg2  11415  fsum3ser  11418  fsumcl2lem  11419  fsumadd  11427  sumsnf  11430  fsummulc2  11469  isumlessdc  11517  cbvprod  11579  prodrbdclem  11592  prodmodclem3  11596  prodmodclem2a  11597  prodmodc  11599  zproddc  11600  fprodseq  11604  fprodntrivap  11605  prodssdc  11610  fprodmul  11612  prodsnf  11613  pcmpt  12354  pcmptdvds  12356  lgsval  14645  lgsfvalg  14646  lgsdir  14676  lgsdilem2  14677  lgsdi  14678  lgsne0  14679