![]() |
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 4313 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2784 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 475 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 224 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4316 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2784 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 475 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 224 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 803 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ifcif 4307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-if 4308 |
This theorem is referenced by: ifboth 4345 resixpfo 8232 boxriin 8236 boxcutc 8237 suppr 8665 infpr 8697 cantnflem1 8883 ttukeylem5 9670 ttukeylem6 9671 bitsinv1lem 15569 bitsinv1 15570 smumullem 15620 hashgcdeq 15898 ramcl2lem 16117 acsfn 16705 tsrlemax 17606 odlem1 18338 gexlem1 18378 cyggex2 18684 dprdfeq0 18808 mplmon2 19889 evlslem1 19911 coe1tmmul2 20042 coe1tmmul 20043 xrsdsreclb 20189 ptcld 21825 xkopt 21867 stdbdxmet 22728 xrsxmet 23020 iccpnfcnv 23151 iccpnfhmeo 23152 xrhmeo 23153 dvcobr 24146 mdegle0 24274 dvradcnv 24612 psercnlem1 24616 psercn 24617 logtayl 24843 efrlim 25148 lgamgulmlem5 25211 musum 25369 dchrmulid2 25429 dchrsum2 25445 sumdchr2 25447 dchrisum0flblem1 25649 dchrisum0flblem2 25650 rplogsum 25668 pntlemj 25744 eupth2lem1 27622 eulerpathpr 27644 ifeqeqx 29924 xrge0iifcnv 30577 xrge0iifhom 30581 esumpinfval 30733 dstfrvunirn 31135 sgn3da 31202 plymulx0 31224 signswn0 31237 signswch 31238 fnejoin2 32952 poimirlem16 34051 poimirlem17 34052 poimirlem19 34054 poimirlem20 34055 poimirlem24 34059 cnambfre 34083 itg2addnclem 34086 itg2addnclem3 34088 itg2addnc 34089 itg2gt0cn 34090 ftc1anclem7 34116 ftc1anclem8 34117 ftc1anc 34118 kelac1 38592 |
Copyright terms: Public domain | W3C validator |