Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dedth3h | Structured version Visualization version GIF version |
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4090. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
dedth3h.1 | ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏)) |
dedth3h.2 | ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂)) |
dedth3h.3 | ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁)) |
dedth3h.4 | ⊢ 𝜁 |
Ref | Expression |
---|---|
dedth3h | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedth3h.1 | . . . 4 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (𝜃 ↔ 𝜏)) | |
2 | 1 | imbi2d 329 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜓 ∧ 𝜒) → 𝜏))) |
3 | dedth3h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂)) | |
4 | dedth3h.3 | . . . 4 ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁)) | |
5 | dedth3h.4 | . . . 4 ⊢ 𝜁 | |
6 | 3, 4, 5 | dedth2h 4090 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜏) |
7 | 2, 6 | dedth 4089 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
8 | 7 | 3impib 1254 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = 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-3an 1033 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: dedth3v 4094 faclbnd4lem2 12943 dvdsle 14870 gcdaddm 15084 ipdiri 27069 hvaddcan 27311 hvsubadd 27318 norm3dif 27391 omlsii 27646 chjass 27776 ledi 27783 spansncv 27896 pjcjt2 27935 pjopyth 27963 hoaddass 28025 hocsubdir 28028 hoddi 28233 |
Copyright terms: Public domain | W3C validator |