Theorem ifan 4582

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 4535	. . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2		ibar 527	. . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	2	ifbid 4552	. . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵))
4	1, 3	eqtr2d 2771	. 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5		simpl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
6	5	con3i 154	. . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
7	6	iffalsed 4540	. . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵)
8		iffalse 4538	. . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
9	7, 8	eqtr4d 2773	. 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
10	4, 9	pm2.61i 182	1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 394   = wceq 1539  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4530

This theorem is referenced by:  itg0  25531  iblre  25545  itgreval  25548  iblss  25556  iblss2  25557  itgle  25561  itgss  25563  itgeqa  25565  iblconst  25569  itgconst  25570  ibladdlem  25571  iblabslem  25579  iblabsr  25581  iblmulc2  25582  itgsplit  25587  bddiblnc  25593  itgcn  25596  mrsubrn  34800  itg2gt0cn  36848  ibladdnclem  36849  iblabsnclem  36856  iblmulc2nc  36858  selvvvval  41461  iblsplit  44982