![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifan | Structured version Visualization version GIF version |
Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014.) |
Ref | Expression |
---|---|
ifan | ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftrue 4530 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
2 | ibar 528 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 2 | ifbid 4547 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
4 | 1, 3 | eqtr2d 2768 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
5 | simpl 482 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
6 | 5 | con3i 154 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
7 | 6 | iffalsed 4535 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
8 | iffalse 4533 | . . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵) | |
9 | 7, 8 | eqtr4d 2770 | . 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
10 | 4, 9 | pm2.61i 182 | 1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 395 = wceq 1534 ifcif 4524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-if 4525 |
This theorem is referenced by: itg0 25696 iblre 25710 itgreval 25713 iblss 25721 iblss2 25722 itgle 25726 itgss 25728 itgeqa 25730 iblconst 25734 itgconst 25735 ibladdlem 25736 iblabslem 25744 iblabsr 25746 iblmulc2 25747 itgsplit 25752 bddiblnc 25758 itgcn 25761 mrsubrn 35059 itg2gt0cn 37083 ibladdnclem 37084 iblabsnclem 37091 iblmulc2nc 37093 selvvvval 41740 iblsplit 45277 |
Copyright terms: Public domain | W3C validator |