Theorem mpidan 688

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  funopsn  7146  oeoelem  8598  qsdisj  8788  faclbnd4lem4  14256  sumrb  15659  prodrblem2  15875  pwspjmhmmgpd  20141  asclpropd  21451  tx2cn  23114  ustuqtop5  23750  iocopnst  24456  cmetcaulem  24805  dvaddbr  25455  dvmulbr  25456  tglineeltr  27913  wlkp1lem6  28966  upgr1wlkdlem2  29430  grplsm0l  32544  ressply1invg  32689  gg-dvmulbr  35206  poimirlem17  36553  poimirlem20  36556  rngonegmn1l  36857  qsdisjALTV  37533  mplmapghm  41176  naddcnfid1  42165  icccncfext  44651  isomuspgrlem2c  46546