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 4523. (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 343 | . . 3 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐷) → (((𝜓 ∧ 𝜒) → 𝜃) ↔ ((𝜓 ∧ 𝜒) → 𝜏))) |
3 | dedth3h.2 | . . . 4 ⊢ (𝐵 = if(𝜓, 𝐵, 𝑅) → (𝜏 ↔ 𝜂)) | |
4 | dedth3h.3 | . . . 4 ⊢ (𝐶 = if(𝜒, 𝐶, 𝑆) → (𝜂 ↔ 𝜁)) | |
5 | dedth3h.4 | . . . 4 ⊢ 𝜁 | |
6 | 3, 4, 5 | dedth2h 4523 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜏) |
7 | 2, 6 | dedth 4522 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
8 | 7 | 3impib 1112 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ifcif 4466 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-ex 1777 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-if 4467 |
This theorem is referenced by: dedth3v 4527 faclbnd4lem2 13653 dvdsle 15659 gcdaddm 15872 ipdiri 28606 hvaddcan 28846 hvsubadd 28853 norm3dif 28926 omlsii 29179 chjass 29309 ledi 29316 spansncv 29429 pjcjt2 29468 pjopyth 29496 hoaddass 29558 hocsubdir 29561 hoddi 29766 |
Copyright terms: Public domain | W3C validator |