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 4473 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
2 | ibar 531 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 2 | ifbid 4489 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
4 | 1, 3 | eqtr2d 2857 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
5 | simpl 485 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
6 | 5 | con3i 157 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
7 | 6 | iffalsed 4478 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
8 | iffalse 4476 | . . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵) | |
9 | 7, 8 | eqtr4d 2859 | . 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
10 | 4, 9 | pm2.61i 184 | 1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 398 = wceq 1537 ifcif 4467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-if 4468 |
This theorem is referenced by: itg0 24380 iblre 24394 itgreval 24397 iblss 24405 iblss2 24406 itgle 24410 itgss 24412 itgeqa 24414 iblconst 24418 itgconst 24419 ibladdlem 24420 iblabslem 24428 iblabsr 24430 iblmulc2 24431 itgsplit 24436 itgcn 24443 mrsubrn 32760 itg2gt0cn 34962 ibladdnclem 34963 iblabsnclem 34970 iblmulc2nc 34972 bddiblnc 34977 iblsplit 42271 |
Copyright terms: Public domain | W3C validator |