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  7082  oeoelem  8516  qsdisj  8721  faclbnd4lem4  14203  sumrb  15620  prodrblem2  15838  pwspjmhmmgpd  20213  asclpropd  21804  psdmvr  22054  tx2cn  23495  ustuqtop5  24131  iocopnst  24835  cmetcaulem  25186  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  tglineeltr  28576  wlkp1lem6  29622  upgr1wlkdlem2  30090  grplsm0l  33340  ressply1invg  33504  poimirlem17  37621  poimirlem20  37624  rngonegmn1l  37925  qsdisjALTV  38596  mplmapghm  42533  naddcnfid1  43344  icccncfext  45872  isubgr3stgrlem7  47960  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112