Theorem mpidan 702

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 486	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpidan.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpdan 700	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  funopsnOLD  7182  oeoelem  8643  qsdisj  8851  faclbnd4lem4  14479  sumrb  15920  prodrblem2  16139  pwspjmhmmgpd  20599  asclpropd  22249  mplmapghm  22475  psdmvr  22534  tx2cn  23973  ustuqtop5  24608  iocopnst  25305  cmetcaulem  25653  dvaddbr  26302  dvmulbr  26303  tglineeltr  29145  wlkp1lem6  30303  upgr1wlkdlem2  30783  grplsm0l  34051  ressply1invg  34197  mplvrpmmhm  34282  mplvrpmrhm  34283  poimirlem17  38816  poimirlem20  38819  rngonegmn1l  39134  qsdisjALTV  39890  naddcnfid1  44624  icccncfext  47164  isubgr3stgrlem7  49337  pgnbgreunbgrlem3  49483  pgnbgreunbgrlem6  49489