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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  funopsn  6887  oeoelem  8207  qsdisj  8357  faclbnd4lem4  13652  sumrb  15062  prodrblem2  15277  asclpropd  20583  tx2cn  22215  ustuqtop5  22851  iocopnst  23545  cmetcaulem  23892  dvaddbr  24541  dvmulbr  24542  tglineeltr  26425  wlkp1lem6  27468  upgr1wlkdlem2  27931  poimirlem17  35074  poimirlem20  35077  rngonegmn1l  35379  qsdisjALTV  36010  icccncfext  42529  isomuspgrlem2c  44348