Theorem ifan 4535

Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.)

Assertion

Ref	Expression
ifan	⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

Proof of Theorem ifan

Step	Hyp	Ref	Expression
1		iftrue 4487	. . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2		ibar 538	. . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	2	ifbid 4505	. . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵))
4	1, 3	eqtr2d 2796	. 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5		simpl 488	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
6	5	con3i 155	. . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
7	6	iffalsed 4492	. . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵)
8		iffalse 4490	. . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
9	7, 8	eqtr4d 2798	. 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
10	4, 9	pm2.61i 184	1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  selvvvval  22412  psdmvr  22451  itg0  26061  iblre  26075  itgreval  26078  iblss  26086  iblss2  26087  itgle  26091  itgss  26093  itgeqa  26095  iblconst  26099  itgconst  26100  ibladdlem  26101  iblabslem  26109  iblabsr  26111  iblmulc2  26112  itgsplit  26117  bddiblnc  26123  itgcn  26126  ififcom  33079  esplyfv  34135  esplyfval3  34137  mrsubrn  36199  itg2gt0cn  38513  ibladdnclem  38514  iblabsnclem  38521  iblmulc2nc  38523  iblsplit  46898