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  7102  oeoelem  8539  qsdisj  8744  faclbnd4lem4  14237  sumrb  15655  prodrblem2  15873  pwspjmhmmgpd  20213  asclpropd  21782  psdmvr  22032  tx2cn  23473  ustuqtop5  24109  iocopnst  24813  cmetcaulem  25164  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  tglineeltr  28534  wlkp1lem6  29580  upgr1wlkdlem2  30048  grplsm0l  33347  ressply1invg  33511  poimirlem17  37604  poimirlem20  37607  rngonegmn1l  37908  qsdisjALTV  38579  mplmapghm  42517  naddcnfid1  43329  icccncfext  45858  isubgr3stgrlem7  47944  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem6  48087