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 4042 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
3 | 2 | eqcomd 2616 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) |
4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
6 | 5 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) |
7 | 1, 6 | mpbid 221 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) |
8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
9 | iffalse 4045 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
10 | 9 | eqcomd 2616 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) |
11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) |
13 | 12 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) |
14 | 8, 13 | mpbid 221 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) |
15 | 7, 14 | pm2.61dan 828 | 1 ⊢ (𝜂 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ifcif 4036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-if 4037 |
This theorem is referenced by: ifboth 4074 resixpfo 7832 boxriin 7836 boxcutc 7837 suppr 8260 infpr 8292 cantnflem1 8469 ttukeylem5 9218 ttukeylem6 9219 bitsinv1lem 15001 bitsinv1 15002 smumullem 15052 hashgcdeq 15332 ramcl2lem 15551 acsfn 16143 tsrlemax 17043 odlem1 17777 gexlem1 17817 cyggex2 18121 dprdfeq0 18244 mplmon2 19314 evlslem1 19336 coe1tmmul2 19467 coe1tmmul 19468 xrsdsreclb 19612 ptcld 21226 xkopt 21268 stdbdxmet 22130 xrsxmet 22420 iccpnfcnv 22551 iccpnfhmeo 22552 xrhmeo 22553 dvcobr 23515 mdegle0 23641 dvradcnv 23979 psercnlem1 23983 psercn 23984 logtayl 24206 efrlim 24496 lgamgulmlem5 24559 musum 24717 dchrmulid2 24777 dchrsum2 24793 sumdchr2 24795 dchrisum0flblem1 24997 dchrisum0flblem2 24998 rplogsum 25016 pntlemj 25092 eupath2lem1 26504 eupath 26508 ifeqeqx 28745 xrge0iifcnv 29307 xrge0iifhom 29311 esumpinfval 29462 dstfrvunirn 29863 sgn3da 29930 plymulx0 29950 signswn0 29963 signswch 29964 fnejoin2 31534 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem24 32603 cnambfre 32628 itg2addnclem 32631 itg2addnclem3 32633 itg2addnc 32634 itg2gt0cn 32635 ftc1anclem7 32661 ftc1anclem8 32662 ftc1anc 32663 kelac1 36651 eupth2lem1 41386 eulerpathpr 41408 |
Copyright terms: Public domain | W3C validator |