![]() |
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 4529 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2732 | . . . . 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 4532 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2732 | . . . . 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 4523 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-if 4524 |
This theorem is referenced by: ifboth 4562 resixpfo 8932 boxriin 8936 boxcutc 8937 suppr 9468 infpr 9500 cantnflem1 9686 ttukeylem5 10510 ttukeylem6 10511 bitsinv1lem 16389 bitsinv1 16390 smumullem 16440 hashgcdeq 16731 ramcl2lem 16951 acsfn 17612 tsrlemax 18551 odlem1 19455 gexlem1 19499 cyggex2 19817 dprdfeq0 19944 xrsdsreclb 21307 mplmon2 21964 evlslem1 21987 coe1tmmul2 22150 coe1tmmul 22151 ptcld 23472 xkopt 23514 stdbdxmet 24379 xrsxmet 24680 iccpnfcnv 24824 iccpnfhmeo 24825 xrhmeo 24826 dvcobr 25832 dvcobrOLD 25833 mdegle0 25968 dvradcnv 26312 psercnlem1 26317 psercn 26318 logtayl 26549 efrlim 26856 efrlimOLD 26857 lgamgulmlem5 26920 musum 27078 dchrmullid 27140 dchrsum2 27156 sumdchr2 27158 dchrisum0flblem1 27396 dchrisum0flblem2 27397 rplogsum 27415 pntlemj 27491 eupth2lem1 29980 eulerpathpr 30002 ifeqeqx 32283 xrge0iifcnv 33443 xrge0iifhom 33447 esumpinfval 33601 dstfrvunirn 34003 sgn3da 34070 plymulx0 34088 signswn0 34101 signswch 34102 lpadmax 34223 lpadright 34225 fnejoin2 35762 poimirlem16 37017 poimirlem17 37018 poimirlem19 37020 poimirlem20 37021 poimirlem24 37025 cnambfre 37049 itg2addnclem 37052 itg2addnclem3 37054 itg2addnc 37055 itg2gt0cn 37056 ftc1anclem7 37080 ftc1anclem8 37081 ftc1anc 37082 sticksstones10 41532 sticksstones12a 41534 metakunt1 41546 metakunt2 41547 metakunt25 41570 kelac1 42383 |
Copyright terms: Public domain | W3C validator |