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

Theorem mpidan 701
 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 480 . 2 ((𝜑𝜓) → 𝜒)
3 mpidan.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3mpdan 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