Theorem mpidan 689

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  funopsn  7076  oeoelem  8508  qsdisj  8713  faclbnd4lem4  14198  sumrb  15615  prodrblem2  15833  pwspjmhmmgpd  20241  asclpropd  21829  psdmvr  22079  tx2cn  23520  ustuqtop5  24155  iocopnst  24859  cmetcaulem  25210  dvaddbr  25862  dvmulbr  25863  dvmulbrOLD  25864  tglineeltr  28604  wlkp1lem6  29650  upgr1wlkdlem2  30118  grplsm0l  33360  ressply1invg  33524  mplvrpmmhm  33568  mplvrpmrhm  33569  poimirlem17  37677  poimirlem20  37680  rngonegmn1l  37981  qsdisjALTV  38652  mplmapghm  42589  naddcnfid1  43400  icccncfext  45925  isubgr3stgrlem7  48003  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155