![]() |
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 4431 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
2 | ibar 532 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 2 | ifbid 4447 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
4 | 1, 3 | eqtr2d 2834 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
5 | simpl 486 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
6 | 5 | con3i 157 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
7 | 6 | iffalsed 4436 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
8 | iffalse 4434 | . . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵) | |
9 | 7, 8 | eqtr4d 2836 | . 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
10 | 4, 9 | pm2.61i 185 | 1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 399 = wceq 1538 ifcif 4425 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-if 4426 |
This theorem is referenced by: itg0 24383 iblre 24397 itgreval 24400 iblss 24408 iblss2 24409 itgle 24413 itgss 24415 itgeqa 24417 iblconst 24421 itgconst 24422 ibladdlem 24423 iblabslem 24431 iblabsr 24433 iblmulc2 24434 itgsplit 24439 bddiblnc 24445 itgcn 24448 mrsubrn 32873 itg2gt0cn 35112 ibladdnclem 35113 iblabsnclem 35120 iblmulc2nc 35122 iblsplit 42608 |
Copyright terms: Public domain | W3C validator |