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 4465 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2744 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 482 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 231 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4468 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2744 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 482 | . . 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 396 = wceq 1539 ifcif 4459 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-if 4460 |
This theorem is referenced by: ifboth 4498 resixpfo 8724 boxriin 8728 boxcutc 8729 suppr 9230 infpr 9262 cantnflem1 9447 ttukeylem5 10269 ttukeylem6 10270 bitsinv1lem 16148 bitsinv1 16149 smumullem 16199 hashgcdeq 16490 ramcl2lem 16710 acsfn 17368 tsrlemax 18304 odlem1 19143 gexlem1 19184 cyggex2 19498 dprdfeq0 19625 xrsdsreclb 20645 mplmon2 21269 evlslem1 21292 coe1tmmul2 21447 coe1tmmul 21448 ptcld 22764 xkopt 22806 stdbdxmet 23671 xrsxmet 23972 iccpnfcnv 24107 iccpnfhmeo 24108 xrhmeo 24109 dvcobr 25110 mdegle0 25242 dvradcnv 25580 psercnlem1 25584 psercn 25585 logtayl 25815 efrlim 26119 lgamgulmlem5 26182 musum 26340 dchrmulid2 26400 dchrsum2 26416 sumdchr2 26418 dchrisum0flblem1 26656 dchrisum0flblem2 26657 rplogsum 26675 pntlemj 26751 eupth2lem1 28582 eulerpathpr 28604 ifeqeqx 30885 xrge0iifcnv 31883 xrge0iifhom 31887 esumpinfval 32041 dstfrvunirn 32441 sgn3da 32508 plymulx0 32526 signswn0 32539 signswch 32540 lpadmax 32662 lpadright 32664 fnejoin2 34558 poimirlem16 35793 poimirlem17 35794 poimirlem19 35796 poimirlem20 35797 poimirlem24 35801 cnambfre 35825 itg2addnclem 35828 itg2addnclem3 35830 itg2addnc 35831 itg2gt0cn 35832 ftc1anclem7 35856 ftc1anclem8 35857 ftc1anc 35858 sticksstones10 40111 sticksstones12a 40113 metakunt1 40125 metakunt2 40126 metakunt25 40149 kelac1 40888 |
Copyright terms: Public domain | W3C validator |