| 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 4531 | . . 3 ⊢ (𝜑 → if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵) = if(𝜓, 𝐴, 𝐵)) | |
| 2 | ibar 528 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
| 3 | 2 | ifbid 4549 | . . 3 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if((𝜑 ∧ 𝜓), 𝐴, 𝐵)) |
| 4 | 1, 3 | eqtr2d 2778 | . 2 ⊢ (𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = if(𝜑, if(𝜓, 𝐴, 𝐵), 𝐵)) |
| 5 | simpl 482 | . . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 6 | 5 | con3i 154 | . . . 4 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓)) |
| 7 | 6 | iffalsed 4536 | . . 3 ⊢ (¬ 𝜑 → if((𝜑 ∧ 𝜓), 𝐴, 𝐵) = 𝐵) |
| 8 | iffalse 4534 | . . 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 395 = wceq 1540 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 |
| This theorem is referenced by: psdmvr 22173 itg0 25815 iblre 25829 itgreval 25832 iblss 25840 iblss2 25841 itgle 25845 itgss 25847 itgeqa 25849 iblconst 25853 itgconst 25854 ibladdlem 25855 iblabslem 25863 iblabsr 25865 iblmulc2 25866 itgsplit 25871 bddiblnc 25877 itgcn 25880 mrsubrn 35518 itg2gt0cn 37682 ibladdnclem 37683 iblabsnclem 37690 iblmulc2nc 37692 selvvvval 42595 iblsplit 45981 |
| Copyright terms: Public domain | W3C validator |