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

Theorem mpidan 687
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 685 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  funopsn  7090  oeoelem  8537  qsdisj  8691  faclbnd4lem4  14150  sumrb  15558  prodrblem2  15774  pwspjmhmmgpd  19996  asclpropd  21253  tx2cn  22913  ustuqtop5  23549  iocopnst  24255  cmetcaulem  24604  dvaddbr  25254  dvmulbr  25255  tglineeltr  27402  wlkp1lem6  28455  upgr1wlkdlem2  28919  grplsm0l  32010  ressply1invg  32099  poimirlem17  36033  poimirlem20  36036  rngonegmn1l  36338  qsdisjALTV  37015  naddcnfid1  41588  icccncfext  44029  isomuspgrlem2c  45923
  Copyright terms: Public domain W3C validator