Theorem mpidan 699

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  funopsnOLD  7126  oeoelem  8562  qsdisj  8770  faclbnd4lem4  14303  sumrb  15731  prodrblem2  15952  pwspjmhmmgpd  20363  asclpropd  21937  mplmapghm  22163  psdmvr  22222  tx2cn  23658  ustuqtop5  24293  iocopnst  24990  cmetcaulem  25338  dvaddbr  25988  dvmulbr  25989  tglineeltr  28788  wlkp1lem6  29834  upgr1wlkdlem2  30305  grplsm0l  33550  ressply1invg  33726  mplvrpmmhm  33804  mplvrpmrhm  33805  poimirlem17  38097  poimirlem20  38100  rngonegmn1l  38401  qsdisjALTV  39159  naddcnfid1  43905  icccncfext  46422  isubgr3stgrlem7  48555  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem6  48707