Theorem mpidan 701

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  funopsnOLD  7145  oeoelem  8580  qsdisj  8788  faclbnd4lem4  14328  sumrb  15760  prodrblem2  15981  pwspjmhmmgpd  20405  asclpropd  22047  mplmapghm  22273  psdmvr  22332  tx2cn  23767  ustuqtop5  24402  iocopnst  25099  cmetcaulem  25447  dvaddbr  26097  dvmulbr  26098  tglineeltr  28904  wlkp1lem6  30026  upgr1wlkdlem2  30497  grplsm0l  33712  ressply1invg  33859  mplvrpmmhm  33936  mplvrpmrhm  33937  poimirlem17  38288  poimirlem20  38291  rngonegmn1l  38592  qsdisjALTV  39348  naddcnfid1  44094  icccncfext  46601  isubgr3stgrlem7  48737  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem6  48889