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

Theorem mpidan 689
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 687 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  funopsn  7168  oeoelem  8636  qsdisj  8834  faclbnd4lem4  14335  sumrb  15749  prodrblem2  15967  pwspjmhmmgpd  20325  asclpropd  21917  psdmvr  22173  tx2cn  23618  ustuqtop5  24254  iocopnst  24970  cmetcaulem  25322  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  tglineeltr  28639  wlkp1lem6  29696  upgr1wlkdlem2  30165  grplsm0l  33431  ressply1invg  33594  poimirlem17  37644  poimirlem20  37647  rngonegmn1l  37948  qsdisjALTV  38616  mplmapghm  42566  naddcnfid1  43380  icccncfext  45902  isubgr3stgrlem7  47939
  Copyright terms: Public domain W3C validator