|   | 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 4531 | . . . . . 6 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
| 3 | 2 | eqcomd 2743 | . . . . 5 ⊢ (𝜑 → 𝐴 = if(𝜑, 𝐴, 𝐵)) | 
| 4 | ifboth.1 | . . . . 5 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃)) | |
| 5 | 3, 4 | syl 17 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | 
| 6 | 5 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ 𝜑) → (𝜓 ↔ 𝜃)) | 
| 7 | 1, 6 | mpbid 232 | . 2 ⊢ ((𝜂 ∧ 𝜑) → 𝜃) | 
| 8 | ifbothda.4 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜒) | |
| 9 | iffalse 4534 | . . . . . 6 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
| 10 | 9 | eqcomd 2743 | . . . . 5 ⊢ (¬ 𝜑 → 𝐵 = if(𝜑, 𝐴, 𝐵)) | 
| 11 | ifboth.2 | . . . . 5 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃)) | |
| 12 | 10, 11 | syl 17 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ 𝜃)) | 
| 13 | 12 | adantl 481 | . . 3 ⊢ ((𝜂 ∧ ¬ 𝜑) → (𝜒 ↔ 𝜃)) | 
| 14 | 8, 13 | mpbid 232 | . 2 ⊢ ((𝜂 ∧ ¬ 𝜑) → 𝜃) | 
| 15 | 7, 14 | pm2.61dan 813 | 1 ⊢ (𝜂 → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ifcif 4525 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-if 4526 | 
| This theorem is referenced by: ifboth 4565 resixpfo 8976 boxriin 8980 boxcutc 8981 suppr 9511 infpr 9543 cantnflem1 9729 ttukeylem5 10553 ttukeylem6 10554 bitsinv1lem 16478 bitsinv1 16479 smumullem 16529 hashgcdeq 16827 ramcl2lem 17047 acsfn 17702 tsrlemax 18631 odlem1 19553 gexlem1 19597 cyggex2 19915 dprdfeq0 20042 xrsdsreclb 21431 mplmon2 22085 evlslem1 22106 coe1tmmul2 22279 coe1tmmul 22280 ptcld 23621 xkopt 23663 stdbdxmet 24528 xrsxmet 24831 iccpnfcnv 24975 iccpnfhmeo 24976 xrhmeo 24977 dvcobr 25983 dvcobrOLD 25984 mdegle0 26116 dvradcnv 26464 psercnlem1 26469 psercn 26470 logtayl 26702 efrlim 27012 efrlimOLD 27013 lgamgulmlem5 27076 musum 27234 dchrmullid 27296 dchrsum2 27312 sumdchr2 27314 dchrisum0flblem1 27552 dchrisum0flblem2 27553 rplogsum 27571 pntlemj 27647 eupth2lem1 30237 eulerpathpr 30259 ifeqeqx 32555 elrgspnlem2 33247 elrgspnlem3 33248 xrge0iifcnv 33932 xrge0iifhom 33936 esumpinfval 34074 dstfrvunirn 34477 sgn3da 34544 plymulx0 34562 signswn0 34575 signswch 34576 lpadmax 34697 lpadright 34699 fnejoin2 36370 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 poimirlem24 37651 cnambfre 37675 itg2addnclem 37678 itg2addnclem3 37680 itg2addnc 37681 itg2gt0cn 37682 ftc1anclem7 37706 ftc1anclem8 37707 ftc1anc 37708 sticksstones10 42156 sticksstones12a 42158 aks6d1c6lem3 42173 metakunt1 42206 metakunt2 42207 metakunt25 42230 kelac1 43075 | 
| Copyright terms: Public domain | W3C validator |