Theorem mpidan 704

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  qsdisj  7824  faclbnd4lem4  13083  sumrb  14444  prodrblem2  14661  asclpropd  19346  tx2cn  21413  ustuqtop5  22049  iocopnst  22739  cmetcaulem  23086  dvaddbr  23701  dvmulbr  23702  tglineeltr  25526  wlkp1lem6  26575  upgr1wlkdlem2  27006  poimirlem17  33426  poimirlem20  33429  rngonegmn1l  33740  icccncfext  40100