Theorem ifbieq1d 3597

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ifcif 3575

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-un 3174  df-if 3576

This theorem is referenced by:  ctssdclemn0  7226  ctssdc  7229  enumctlemm  7230  iseqf1olemfvp  10672  seq3f1olemqsum  10675  seq3f1oleml  10678  seq3f1o  10679  bcval  10911  swrdval  11119  sumrbdclem  11758  summodclem3  11761  summodclem2a  11762  summodc  11764  zsumdc  11765  fsum3  11768  isumss  11772  isumss2  11774  fsum3cvg2  11775  fsum3ser  11778  fsumcl2lem  11779  fsumadd  11787  sumsnf  11790  fsummulc2  11829  isumlessdc  11877  cbvprod  11939  prodrbdclem  11952  prodmodclem3  11956  prodmodclem2a  11957  prodmodc  11959  zproddc  11960  fprodseq  11964  fprodntrivap  11965  prodssdc  11970  fprodmul  11972  prodsnf  11973  pcmpt  12736  pcmptdvds  12738  elply2  15277  lgsval  15551  lgsfvalg  15552  lgsdir  15582  lgsdilem2  15583  lgsdi  15584  lgsne0  15585