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  7153  oeoelem  8611  qsdisj  8819  faclbnd4lem4  14444  sumrb  15885  prodrblem2  16104  pwspjmhmmgpd  20563  asclpropd  22211  mplmapghm  22437  psdmvr  22496  tx2cn  23935  ustuqtop5  24570  iocopnst  25267  cmetcaulem  25615  dvaddbr  26264  dvmulbr  26265  tglineeltr  29105  wlkp1lem6  30263  upgr1wlkdlem2  30743  grplsm0l  34001  ressply1invg  34148  mplvrpmmhm  34225  mplvrpmrhm  34226  poimirlem17  38649  poimirlem20  38652  rngonegmn1l  38969  qsdisjALTV  39725  naddcnfid1  44463  icccncfext  46991  isubgr3stgrlem7  49164  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316