![]() |
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 4493 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
2 | ibar 530 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 2 | ifbid 4510 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
4 | 1, 3 | eqtr2d 2778 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
5 | simpl 484 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
6 | 5 | con3i 154 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
7 | 6 | iffalsed 4498 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
8 | iffalse 4496 | . . 3 ⊢ (¬ 𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = 𝐵) | |
9 | 7, 8 | eqtr4d 2780 | . 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 397 = wceq 1542 ifcif 4487 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-if 4488 |
This theorem is referenced by: itg0 25147 iblre 25161 itgreval 25164 iblss 25172 iblss2 25173 itgle 25177 itgss 25179 itgeqa 25181 iblconst 25185 itgconst 25186 ibladdlem 25187 iblabslem 25195 iblabsr 25197 iblmulc2 25198 itgsplit 25203 bddiblnc 25209 itgcn 25212 mrsubrn 34110 itg2gt0cn 36136 ibladdnclem 36137 iblabsnclem 36144 iblmulc2nc 36146 iblsplit 44214 |
Copyright terms: Public domain | W3C validator |