Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dedth3h | Structured version Visualization version Unicode version |
Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h 4140. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
dedth3h.1 | |
dedth3h.2 | |
dedth3h.3 | |
dedth3h.4 |
Ref | Expression |
---|---|
dedth3h |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dedth3h.1 | . . . 4 | |
2 | 1 | imbi2d 330 | . . 3 |
3 | dedth3h.2 | . . . 4 | |
4 | dedth3h.3 | . . . 4 | |
5 | dedth3h.4 | . . . 4 | |
6 | 3, 4, 5 | dedth2h 4140 | . . 3 |
7 | 2, 6 | dedth 4139 | . 2 |
8 | 7 | 3impib 1262 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 w3a 1037 wceq 1483 cif 4086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-if 4087 |
This theorem is referenced by: dedth3v 4144 faclbnd4lem2 13081 dvdsle 15032 gcdaddm 15246 ipdiri 27685 hvaddcan 27927 hvsubadd 27934 norm3dif 28007 omlsii 28262 chjass 28392 ledi 28399 spansncv 28512 pjcjt2 28551 pjopyth 28579 hoaddass 28641 hocsubdir 28644 hoddi 28849 |
Copyright terms: Public domain | W3C validator |