Theorem mpidan 695

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  funopsnOLD  7091  oeoelem  8524  qsdisj  8731  faclbnd4lem4  14249  sumrb  15666  prodrblem2  15887  pwspjmhmmgpd  20298  asclpropd  21872  mplmapghm  22098  psdmvr  22157  tx2cn  23593  ustuqtop5  24228  iocopnst  24925  cmetcaulem  25273  dvaddbr  25923  dvmulbr  25924  tglineeltr  28717  wlkp1lem6  29763  upgr1wlkdlem2  30234  grplsm0l  33486  ressply1invg  33652  mplvrpmmhm  33730  mplvrpmrhm  33731  poimirlem17  38004  poimirlem20  38007  rngonegmn1l  38308  qsdisjALTV  39066  naddcnfid1  43812  icccncfext  46330  isubgr3stgrlem7  48463  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem6  48615