Theorem mpidan 690

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 688	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:  funopsnOLD  7102  oeoelem  8534  qsdisj  8741  faclbnd4lem4  14258  sumrb  15675  prodrblem2  15896  pwspjmhmmgpd  20307  asclpropd  21877  psdmvr  22135  tx2cn  23575  ustuqtop5  24210  iocopnst  24907  cmetcaulem  25255  dvaddbr  25905  dvmulbr  25906  tglineeltr  28699  wlkp1lem6  29745  upgr1wlkdlem2  30216  grplsm0l  33463  ressply1invg  33629  mplvrpmmhm  33690  mplvrpmrhm  33691  poimirlem17  37958  poimirlem20  37961  rngonegmn1l  38262  qsdisjALTV  39020  mplmapghm  42997  naddcnfid1  43795  icccncfext  46315  isubgr3stgrlem7  48448  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600