MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpidan Structured version   Visualization version   GIF version

Theorem mpidan 703
Description: A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.)
Hypotheses
Ref Expression
mpidan.1 (𝜑𝜒)
mpidan.2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
mpidan ((𝜑𝜓) → 𝜃)

Proof of Theorem mpidan
StepHypRef Expression
1 mpidan.1 . . 3 (𝜑𝜒)
21adantr 481 . 2 ((𝜑𝜓) → 𝜒)
3 mpidan.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3mpdan 701 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  qsdisj  7809  faclbnd4lem4  13066  sumrb  14425  prodrblem2  14642  asclpropd  19327  tx2cn  21394  ustuqtop5  22030  iocopnst  22720  cmetcaulem  23067  dvaddbr  23682  dvmulbr  23683  tglineeltr  25507  wlkp1lem6  26556  upgr1wlkdlem2  26986  poimirlem17  33397  poimirlem20  33400  rngonegmn1l  33711  icccncfext  39863
  Copyright terms: Public domain W3C validator