Theorem ifan 4540

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 4492	. . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2		ibar 537	. . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	2	ifbid 4510	. . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵))
4	1, 3	eqtr2d 2797	. 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5		simpl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
6	5	con3i 155	. . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
7	6	iffalsed 4497	. . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵)
8		iffalse 4495	. . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
9	7, 8	eqtr4d 2799	. 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
10	4, 9	pm2.61i 184	1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487

This theorem is referenced by:  selvvvval  22272  psdmvr  22311  itg0  25918  iblre  25932  itgreval  25935  iblss  25943  iblss2  25944  itgle  25948  itgss  25950  itgeqa  25952  iblconst  25956  itgconst  25957  ibladdlem  25958  iblabslem  25966  iblabsr  25968  iblmulc2  25969  itgsplit  25974  bddiblnc  25980  itgcn  25983  ififcom  32862  esplyfv  33926  esplyfval3  33928  mrsubrn  35959  itg2gt0cn  38270  ibladdnclem  38271  iblabsnclem  38278  iblmulc2nc  38280  iblsplit  46628