Theorem ifeqda 4526

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

Hypotheses

Ref	Expression
ifeqda.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
ifeqda.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)

Assertion

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

Proof of Theorem ifeqda

Step	Hyp	Ref	Expression
1		iftrue 4495	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2804	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4498	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2804	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567  ifcif 4489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4490

This theorem is referenced by:  somincom  6132  cantnfp1  9646  ccatsymb  14616  swrdccat3blem  14772  repswccat  14819  ccatco  14868  bitsinvp1  16503  xrsdsreval  21527  fvmptnn04if  22971  chfacfscmulgsum  22982  chfacfpmmulgsum  22986  oprpiece1res2  25076  phtpycc  25115  plymulidp  26408  atantayl2  27065  ifeq3da  32829  fprodex01  33106  psgnfzto1stlem  33357  fzto1st1  33359  cycpm2tr  33376  elrgspnlem4  33502  elrspunsn  33677  esplyfval1  33904  esplyind  33906  fldextrspunlsp  34005  mdetlap1  34157  madjusmdetlem1  34158  madjusmdetlem2  34159  ccatmulgnn0dir  34873  itgexpif  34934  repr0  34939  elmrsubrn  35907  matunitlindflem1  38150  sticksstones12  42810  redvmptabs  43006  readvrec  43008  frlmvscadiccat  43165  fsuppind  43209  fsuppssindlem1  43210  reabsifneg  44245  reabsifnpos  44246  reabsifpos  44247  reabsifnneg  44248  reabssgn  44249  sqrtcval  44254  mnringmulrcld  44839  fourierdlem101  46808  hoidmv1lelem2  47193  dfafv2  47753  m1modmmod  47985  indprm  48265  indprmfz  48266  linc0scn0  49083  digexp  49267