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  7152  oeoelem  8607  qsdisj  8815  faclbnd4lem4  14440  sumrb  15879  prodrblem2  16098  pwspjmhmmgpd  20557  asclpropd  22205  mplmapghm  22431  psdmvr  22490  tx2cn  23929  ustuqtop5  24564  iocopnst  25261  cmetcaulem  25609  dvaddbr  26258  dvmulbr  26259  tglineeltr  29099  wlkp1lem6  30257  upgr1wlkdlem2  30737  grplsm0l  33954  ressply1invg  34101  mplvrpmmhm  34178  mplvrpmrhm  34179  poimirlem17  38556  poimirlem20  38559  rngonegmn1l  38876  qsdisjALTV  39632  naddcnfid1  44369  icccncfext  46897  isubgr3stgrlem7  49070  pgnbgreunbgrlem3  49216  pgnbgreunbgrlem6  49222