Theorem mpidan 701

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  funopsnOLD  7143  oeoelem  8580  qsdisj  8788  faclbnd4lem4  14328  sumrb  15760  prodrblem2  15981  pwspjmhmmgpd  20405  asclpropd  22012  mplmapghm  22238  psdmvr  22297  tx2cn  23732  ustuqtop5  24367  iocopnst  25064  cmetcaulem  25412  dvaddbr  26062  dvmulbr  26063  tglineeltr  28862  wlkp1lem6  29963  upgr1wlkdlem2  30434  grplsm0l  33652  ressply1invg  33800  mplvrpmmhm  33877  mplvrpmrhm  33878  poimirlem17  38171  poimirlem20  38174  rngonegmn1l  38475  qsdisjALTV  39233  naddcnfid1  43981  icccncfext  46488  isubgr3stgrlem7  48621  pgnbgreunbgrlem3  48767  pgnbgreunbgrlem6  48773