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  7168  oeoelem  8635  qsdisj  8833  faclbnd4lem4  14332  sumrb  15746  prodrblem2  15964  pwspjmhmmgpd  20342  asclpropd  21935  tx2cn  23634  ustuqtop5  24270  iocopnst  24984  cmetcaulem  25336  dvaddbr  25989  dvmulbr  25990  dvmulbrOLD  25991  tglineeltr  28654  wlkp1lem6  29711  upgr1wlkdlem2  30175  grplsm0l  33411  ressply1invg  33574  poimirlem17  37624  poimirlem20  37627  rngonegmn1l  37928  qsdisjALTV  38597  mplmapghm  42543  naddcnfid1  43357  icccncfext  45843  isubgr3stgrlem7  47875