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 4475 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2829 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 484 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 234 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4478 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2829 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 484 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 234 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 811 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ifcif 4469 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-if 4470 |
This theorem is referenced by: ifboth 4507 resixpfo 8502 boxriin 8506 boxcutc 8507 suppr 8937 infpr 8969 cantnflem1 9154 ttukeylem5 9937 ttukeylem6 9938 bitsinv1lem 15792 bitsinv1 15793 smumullem 15843 hashgcdeq 16128 ramcl2lem 16347 acsfn 16932 tsrlemax 17832 odlem1 18665 gexlem1 18706 cyggex2 19019 dprdfeq0 19146 mplmon2 20275 evlslem1 20297 coe1tmmul2 20446 coe1tmmul 20447 xrsdsreclb 20594 ptcld 22223 xkopt 22265 stdbdxmet 23127 xrsxmet 23419 iccpnfcnv 23550 iccpnfhmeo 23551 xrhmeo 23552 dvcobr 24545 mdegle0 24673 dvradcnv 25011 psercnlem1 25015 psercn 25016 logtayl 25245 efrlim 25549 lgamgulmlem5 25612 musum 25770 dchrmulid2 25830 dchrsum2 25846 sumdchr2 25848 dchrisum0flblem1 26086 dchrisum0flblem2 26087 rplogsum 26105 pntlemj 26181 eupth2lem1 27999 eulerpathpr 28021 ifeqeqx 30299 xrge0iifcnv 31178 xrge0iifhom 31182 esumpinfval 31334 dstfrvunirn 31734 sgn3da 31801 plymulx0 31819 signswn0 31832 signswch 31833 lpadmax 31955 lpadright 31957 fnejoin2 33719 poimirlem16 34910 poimirlem17 34911 poimirlem19 34913 poimirlem20 34914 poimirlem24 34918 cnambfre 34942 itg2addnclem 34945 itg2addnclem3 34947 itg2addnc 34948 itg2gt0cn 34949 ftc1anclem7 34975 ftc1anclem8 34976 ftc1anc 34977 kelac1 39670 |
Copyright terms: Public domain | W3C validator |