Theorem ifan 4524

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 4476	. . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵))
2		ibar 535	. . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
3	2	ifbid 4494	. . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵))
4	1, 3	eqtr2d 2788	. 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
5		simpl 485	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
6	5	con3i 154	. . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
7	6	iffalsed 4481	. . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵)
8		iffalse 4479	. . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵)
9	7, 8	eqtr4d 2790	. 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵))
10	4, 9	pm2.61i 183	1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 398   = wceq 1550  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-if 4471

This theorem is referenced by:  selvvvval  22164  psdmvr  22203  itg0  25811  iblre  25825  itgreval  25828  iblss  25836  iblss2  25837  itgle  25841  itgss  25843  itgeqa  25845  iblconst  25849  itgconst  25850  ibladdlem  25851  iblabslem  25859  iblabsr  25861  iblmulc2  25862  itgsplit  25867  bddiblnc  25873  itgcn  25876  ififcom  32687  esplyfv  33811  esplyfval3  33813  mrsubrn  35801  itg2gt0cn  38112  ibladdnclem  38113  iblabsnclem  38120  iblmulc2nc  38122  iblsplit  46478