![]() |
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 4527 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2730 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 231 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4530 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2730 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 231 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 810 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ifcif 4521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-if 4522 |
This theorem is referenced by: ifboth 4560 resixpfo 8927 boxriin 8931 boxcutc 8932 suppr 9463 infpr 9495 cantnflem1 9681 ttukeylem5 10505 ttukeylem6 10506 bitsinv1lem 16381 bitsinv1 16382 smumullem 16432 hashgcdeq 16723 ramcl2lem 16943 acsfn 17604 tsrlemax 18543 odlem1 19447 gexlem1 19491 cyggex2 19809 dprdfeq0 19936 xrsdsreclb 21278 mplmon2 21934 evlslem1 21957 coe1tmmul2 22119 coe1tmmul 22120 ptcld 23441 xkopt 23483 stdbdxmet 24348 xrsxmet 24649 iccpnfcnv 24793 iccpnfhmeo 24794 xrhmeo 24795 dvcobr 25801 dvcobrOLD 25802 mdegle0 25937 dvradcnv 26276 psercnlem1 26281 psercn 26282 logtayl 26513 efrlim 26820 efrlimOLD 26821 lgamgulmlem5 26884 musum 27042 dchrmullid 27104 dchrsum2 27120 sumdchr2 27122 dchrisum0flblem1 27360 dchrisum0flblem2 27361 rplogsum 27379 pntlemj 27455 eupth2lem1 29943 eulerpathpr 29965 ifeqeqx 32246 xrge0iifcnv 33405 xrge0iifhom 33409 esumpinfval 33563 dstfrvunirn 33965 sgn3da 34032 plymulx0 34050 signswn0 34063 signswch 34064 lpadmax 34185 lpadright 34187 fnejoin2 35745 poimirlem16 36998 poimirlem17 36999 poimirlem19 37001 poimirlem20 37002 poimirlem24 37006 cnambfre 37030 itg2addnclem 37033 itg2addnclem3 37035 itg2addnc 37036 itg2gt0cn 37037 ftc1anclem7 37061 ftc1anclem8 37062 ftc1anc 37063 sticksstones10 41468 sticksstones12a 41470 metakunt1 41482 metakunt2 41483 metakunt25 41506 kelac1 42319 |
Copyright terms: Public domain | W3C validator |