Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpidan | Structured version Visualization version GIF version |
Description: A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.) |
Ref | Expression |
---|---|
mpidan.1 | ⊢ (𝜑 → 𝜒) |
mpidan.2 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mpidan | ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpidan.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | mpidan.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mpdan 699 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 |
This theorem is referenced by: qsdisj 7711 faclbnd4lem4 12945 sumrb 14291 prodrblem2 14500 asclpropd 19167 tx2cn 21223 ustuqtop5 21859 iocopnst 22547 cmetcaulem 22894 dvaddbr 23507 dvmulbr 23508 tglineeltr 25326 poimirlem17 32596 poimirlem20 32599 rngonegmn1l 32910 icccncfext 38773 1wlkp1lem6 40887 upgr11wlkdlem2 41313 |
Copyright terms: Public domain | W3C validator |