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 4417 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2744 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 485 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 235 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4420 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2744 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 485 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 235 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 813 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ifcif 4411 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-if 4412 |
This theorem is referenced by: ifboth 4450 resixpfo 8539 boxriin 8543 boxcutc 8544 suppr 9001 infpr 9033 cantnflem1 9218 ttukeylem5 10006 ttukeylem6 10007 bitsinv1lem 15877 bitsinv1 15878 smumullem 15928 hashgcdeq 16219 ramcl2lem 16438 acsfn 17026 tsrlemax 17939 odlem1 18774 gexlem1 18815 cyggex2 19129 dprdfeq0 19256 xrsdsreclb 20257 mplmon2 20866 evlslem1 20889 coe1tmmul2 21044 coe1tmmul 21045 ptcld 22357 xkopt 22399 stdbdxmet 23261 xrsxmet 23554 iccpnfcnv 23689 iccpnfhmeo 23690 xrhmeo 23691 dvcobr 24690 mdegle0 24822 dvradcnv 25160 psercnlem1 25164 psercn 25165 logtayl 25395 efrlim 25699 lgamgulmlem5 25762 musum 25920 dchrmulid2 25980 dchrsum2 25996 sumdchr2 25998 dchrisum0flblem1 26236 dchrisum0flblem2 26237 rplogsum 26255 pntlemj 26331 eupth2lem1 28147 eulerpathpr 28169 ifeqeqx 30451 xrge0iifcnv 31447 xrge0iifhom 31451 esumpinfval 31603 dstfrvunirn 32003 sgn3da 32070 plymulx0 32088 signswn0 32101 signswch 32102 lpadmax 32224 lpadright 32226 fnejoin2 34188 poimirlem16 35405 poimirlem17 35406 poimirlem19 35408 poimirlem20 35409 poimirlem24 35413 cnambfre 35437 itg2addnclem 35440 itg2addnclem3 35442 itg2addnc 35443 itg2gt0cn 35444 ftc1anclem7 35468 ftc1anclem8 35469 ftc1anc 35470 metakunt1 39705 metakunt2 39706 metakunt25 39729 kelac1 40444 |
Copyright terms: Public domain | W3C validator |