![]() |
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 4313 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
2 | ibar 526 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 2 | ifbid 4329 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
4 | 1, 3 | eqtr2d 2863 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
5 | simpl 476 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
6 | 5 | con3i 152 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
7 | 6 | iffalsed 4318 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
8 | iffalse 4316 | . . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵) | |
9 | 7, 8 | eqtr4d 2865 | . 2 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
10 | 4, 9 | pm2.61i 177 | 1 ⊢ if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 386 = wceq 1658 ifcif 4307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2804 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-if 4308 |
This theorem is referenced by: itg0 23946 iblre 23960 itgreval 23963 iblss 23971 iblss2 23972 itgle 23976 itgss 23978 itgeqa 23980 iblconst 23984 itgconst 23985 ibladdlem 23986 iblabslem 23994 iblabsr 23996 iblmulc2 23997 itgsplit 24002 itgcn 24009 mrsubrn 31957 itg2gt0cn 34009 ibladdnclem 34010 iblabsnclem 34017 iblmulc2nc 34019 bddiblnc 34024 iblsplit 40977 |
Copyright terms: Public domain | W3C validator |