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  6910  oeoelem  8224  qsdisj  8374  faclbnd4lem4  13657  sumrb  15070  prodrblem2  15285  asclpropd  20126  tx2cn  22218  ustuqtop5  22854  iocopnst  23544  cmetcaulem  23891  dvaddbr  24535  dvmulbr  24536  tglineeltr  26417  wlkp1lem6  27460  upgr1wlkdlem2  27925  poimirlem17  34924  poimirlem20  34927  rngonegmn1l  35234  qsdisjALTV  35865  icccncfext  42190  isomuspgrlem2c  44015