![]() |
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 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
3 | mpidan.2 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mpdan 685 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: funopsn 7090 oeoelem 8537 qsdisj 8691 faclbnd4lem4 14150 sumrb 15558 prodrblem2 15774 pwspjmhmmgpd 19996 asclpropd 21253 tx2cn 22913 ustuqtop5 23549 iocopnst 24255 cmetcaulem 24604 dvaddbr 25254 dvmulbr 25255 tglineeltr 27402 wlkp1lem6 28455 upgr1wlkdlem2 28919 grplsm0l 32010 ressply1invg 32099 poimirlem17 36033 poimirlem20 36036 rngonegmn1l 36338 qsdisjALTV 37015 naddcnfid1 41588 icccncfext 44029 isomuspgrlem2c 45923 |
Copyright terms: Public domain | W3C validator |