Theorem mpidan 690

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

Step	Hyp	Ref	Expression
1		mpidan.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpidan.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpdan 688	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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  7103  oeoelem  8536  qsdisj  8743  faclbnd4lem4  14231  sumrb  15648  prodrblem2  15866  pwspjmhmmgpd  20275  asclpropd  21865  psdmvr  22124  tx2cn  23566  ustuqtop5  24201  iocopnst  24905  cmetcaulem  25256  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  tglineeltr  28715  wlkp1lem6  29762  upgr1wlkdlem2  30233  grplsm0l  33496  ressply1invg  33662  mplvrpmmhm  33723  mplvrpmrhm  33724  poimirlem17  37888  poimirlem20  37891  rngonegmn1l  38192  qsdisjALTV  38950  mplmapghm  42922  naddcnfid1  43724  icccncfext  46245  isubgr3stgrlem7  48332  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem6  48484