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 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  selvvvval  22451  psdmvr  22490  itg0  26100  iblre  26114  itgreval  26117  iblss  26125  iblss2  26126  itgle  26130  itgss  26132  itgeqa  26134  iblconst  26138  itgconst  26139  ibladdlem  26140  iblabslem  26148  iblabsr  26150  iblmulc2  26151  itgsplit  26156  bddiblnc  26162  itgcn  26165  ififcom  33188  esplyfv  34244  esplyfval3  34246  mrsubrn  36320  itg2gt0cn  38636  ibladdnclem  38637  iblabsnclem  38644  iblmulc2nc  38646  iblsplit  47019