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

Theorem mpidan 679
 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 474 . 2 ((𝜑𝜓) → 𝜒)
3 mpidan.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3mpdan 677 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386 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 199  df-an 387 This theorem is referenced by:  funopsn  6679  oeoelem  7962  qsdisj  8107  faclbnd4lem4  13401  sumrb  14851  prodrblem2  15064  asclpropd  19743  tx2cn  21822  ustuqtop5  22457  iocopnst  23147  cmetcaulem  23494  dvaddbr  24138  dvmulbr  24139  tglineeltr  25982  wlkp1lem6  27029  upgr1wlkdlem2  27549  poimirlem17  34052  poimirlem20  34055  rngonegmn1l  34364  qsdisjALTV  34985  icccncfext  41028  isomuspgrlem2c  42743
 Copyright terms: Public domain W3C validator