Theorem mpidan 687

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  funopsn  6912  oeoelem  8226  qsdisj  8376  faclbnd4lem4  13659  sumrb  15072  prodrblem2  15287  asclpropd  20128  tx2cn  22220  ustuqtop5  22856  iocopnst  23546  cmetcaulem  23893  dvaddbr  24537  dvmulbr  24538  tglineeltr  26419  wlkp1lem6  27462  upgr1wlkdlem2  27927  poimirlem17  34911  poimirlem20  34914  rngonegmn1l  35221  qsdisjALTV  35852  icccncfext  42177  isomuspgrlem2c  44002