|   | 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 687 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: funopsn 7168 oeoelem 8636 qsdisj 8834 faclbnd4lem4 14335 sumrb 15749 prodrblem2 15967 pwspjmhmmgpd 20325 asclpropd 21917 psdmvr 22173 tx2cn 23618 ustuqtop5 24254 iocopnst 24970 cmetcaulem 25322 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 tglineeltr 28639 wlkp1lem6 29696 upgr1wlkdlem2 30165 grplsm0l 33431 ressply1invg 33594 poimirlem17 37644 poimirlem20 37647 rngonegmn1l 37948 qsdisjALTV 38616 mplmapghm 42566 naddcnfid1 43380 icccncfext 45902 isubgr3stgrlem7 47939 | 
| Copyright terms: Public domain | W3C validator |