![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifbothda | Structured version Visualization version GIF version |
Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015.) |
Ref | Expression |
---|---|
ifboth.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) |
ifboth.2 | ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) |
ifbothda.3 | ⊢ ((𝜂 ∧ 𝜑) → 𝜓) |
ifbothda.4 | ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) |
Ref | Expression |
---|---|
ifbothda | ⊢ (𝜂 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ifbothda.3 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → 𝜓) | |
2 | iftrue 4125 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2657 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 222 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4128 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2657 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 222 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 849 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ifcif 4119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-if 4120 |
This theorem is referenced by: ifboth 4157 resixpfo 7988 boxriin 7992 boxcutc 7993 suppr 8418 infpr 8450 cantnflem1 8624 ttukeylem5 9373 ttukeylem6 9374 bitsinv1lem 15210 bitsinv1 15211 smumullem 15261 hashgcdeq 15541 ramcl2lem 15760 acsfn 16367 tsrlemax 17267 odlem1 18000 gexlem1 18040 cyggex2 18344 dprdfeq0 18467 mplmon2 19541 evlslem1 19563 coe1tmmul2 19694 coe1tmmul 19695 xrsdsreclb 19841 ptcld 21464 xkopt 21506 stdbdxmet 22367 xrsxmet 22659 iccpnfcnv 22790 iccpnfhmeo 22791 xrhmeo 22792 dvcobr 23754 mdegle0 23882 dvradcnv 24220 psercnlem1 24224 psercn 24225 logtayl 24451 efrlim 24741 lgamgulmlem5 24804 musum 24962 dchrmulid2 25022 dchrsum2 25038 sumdchr2 25040 dchrisum0flblem1 25242 dchrisum0flblem2 25243 rplogsum 25261 pntlemj 25337 eupth2lem1 27196 eulerpathpr 27218 ifeqeqx 29487 xrge0iifcnv 30107 xrge0iifhom 30111 esumpinfval 30263 dstfrvunirn 30664 sgn3da 30731 plymulx0 30752 signswn0 30765 signswch 30766 fnejoin2 32489 poimirlem16 33555 poimirlem17 33556 poimirlem19 33558 poimirlem20 33559 poimirlem24 33563 cnambfre 33588 itg2addnclem 33591 itg2addnclem3 33593 itg2addnc 33594 itg2gt0cn 33595 ftc1anclem7 33621 ftc1anclem8 33622 ftc1anc 33623 kelac1 37950 |
Copyright terms: Public domain | W3C validator |