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

Theorem mpidan 688
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 484 . 2 ((𝜑𝜓) → 𝜒)
3 mpidan.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3mpdan 686 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  funopsn  6892  oeoelem  8211  qsdisj  8361  faclbnd4lem4  13652  sumrb  15061  prodrblem2  15276  asclpropd  20581  tx2cn  22213  ustuqtop5  22849  iocopnst  23543  cmetcaulem  23890  dvaddbr  24539  dvmulbr  24540  tglineeltr  26423  wlkp1lem6  27466  upgr1wlkdlem2  27929  poimirlem17  35033  poimirlem20  35036  rngonegmn1l  35338  qsdisjALTV  35969  icccncfext  42469  isomuspgrlem2c  44288
  Copyright terms: Public domain W3C validator