Theorem mpidan 702

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  funopsnOLD  7149  oeoelem  8586  qsdisj  8794  faclbnd4lem4  14346  sumrb  15783  prodrblem2  16004  pwspjmhmmgpd  20435  asclpropd  22077  mplmapghm  22303  psdmvr  22362  tx2cn  23798  ustuqtop5  24433  iocopnst  25130  cmetcaulem  25478  dvaddbr  26128  dvmulbr  26129  tglineeltr  28935  wlkp1lem6  30060  upgr1wlkdlem2  30540  grplsm0l  33752  ressply1invg  33899  mplvrpmmhm  33976  mplvrpmrhm  33977  poimirlem17  38321  poimirlem20  38324  rngonegmn1l  38625  qsdisjALTV  39381  naddcnfid1  44127  icccncfext  46634  isubgr3stgrlem7  48770  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922