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  7145  oeoelem  8586  qsdisj  8794  faclbnd4lem4  14360  sumrb  15799  prodrblem2  16018  pwspjmhmmgpd  20468  asclpropd  22112  mplmapghm  22338  psdmvr  22397  tx2cn  23836  ustuqtop5  24471  iocopnst  25168  cmetcaulem  25516  dvaddbr  26165  dvmulbr  26166  tglineeltr  28978  wlkp1lem6  30136  upgr1wlkdlem2  30616  grplsm0l  33832  ressply1invg  33979  mplvrpmmhm  34056  mplvrpmrhm  34057  poimirlem17  38386  poimirlem20  38389  rngonegmn1l  38691  qsdisjALTV  39447  naddcnfid1  44208  icccncfext  46715  isubgr3stgrlem7  48888  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040