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  7150  oeoelem  8600  qsdisj  8808  faclbnd4lem4  14433  sumrb  15872  prodrblem2  16091  pwspjmhmmgpd  20550  asclpropd  22198  mplmapghm  22424  psdmvr  22483  tx2cn  23922  ustuqtop5  24557  iocopnst  25254  cmetcaulem  25602  dvaddbr  26251  dvmulbr  26252  tglineeltr  29092  wlkp1lem6  30250  upgr1wlkdlem2  30730  grplsm0l  33947  ressply1invg  34094  mplvrpmmhm  34171  mplvrpmrhm  34172  poimirlem17  38535  poimirlem20  38538  rngonegmn1l  38855  qsdisjALTV  39611  naddcnfid1  44353  icccncfext  46866  isubgr3stgrlem7  49039  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191