Theorem mpidan 679

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  funopsn  6679  oeoelem  7962  qsdisj  8107  faclbnd4lem4  13401  sumrb  14851  prodrblem2  15064  asclpropd  19743  tx2cn  21822  ustuqtop5  22457  iocopnst  23147  cmetcaulem  23494  dvaddbr  24138  dvmulbr  24139  tglineeltr  25982  wlkp1lem6  27029  upgr1wlkdlem2  27549  poimirlem17  34052  poimirlem20  34055  rngonegmn1l  34364  qsdisjALTV  34985  icccncfext  41028  isomuspgrlem2c  42743