![]() |
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 4493 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2743 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 483 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 231 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4496 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2743 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 483 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 231 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 812 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ifcif 4487 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-if 4488 |
This theorem is referenced by: ifboth 4526 resixpfo 8875 boxriin 8879 boxcutc 8880 suppr 9408 infpr 9440 cantnflem1 9626 ttukeylem5 10450 ttukeylem6 10451 bitsinv1lem 16322 bitsinv1 16323 smumullem 16373 hashgcdeq 16662 ramcl2lem 16882 acsfn 17540 tsrlemax 18476 odlem1 19318 gexlem1 19362 cyggex2 19675 dprdfeq0 19802 xrsdsreclb 20847 mplmon2 21472 evlslem1 21495 coe1tmmul2 21650 coe1tmmul 21651 ptcld 22967 xkopt 23009 stdbdxmet 23874 xrsxmet 24175 iccpnfcnv 24310 iccpnfhmeo 24311 xrhmeo 24312 dvcobr 25313 mdegle0 25445 dvradcnv 25783 psercnlem1 25787 psercn 25788 logtayl 26018 efrlim 26322 lgamgulmlem5 26385 musum 26543 dchrmulid2 26603 dchrsum2 26619 sumdchr2 26621 dchrisum0flblem1 26859 dchrisum0flblem2 26860 rplogsum 26878 pntlemj 26954 eupth2lem1 29165 eulerpathpr 29187 ifeqeqx 31467 xrge0iifcnv 32517 xrge0iifhom 32521 esumpinfval 32675 dstfrvunirn 33077 sgn3da 33144 plymulx0 33162 signswn0 33175 signswch 33176 lpadmax 33298 lpadright 33300 fnejoin2 34844 poimirlem16 36097 poimirlem17 36098 poimirlem19 36100 poimirlem20 36101 poimirlem24 36105 cnambfre 36129 itg2addnclem 36132 itg2addnclem3 36134 itg2addnc 36135 itg2gt0cn 36136 ftc1anclem7 36160 ftc1anclem8 36161 ftc1anc 36162 sticksstones10 40566 sticksstones12a 40568 metakunt1 40580 metakunt2 40581 metakunt25 40604 kelac1 41393 |
Copyright terms: Public domain | W3C validator |