Theorem mpidan 689

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  funopsn  7086  oeoelem  8523  qsdisj  8728  faclbnd4lem4  14222  sumrb  15639  prodrblem2  15857  pwspjmhmmgpd  20232  asclpropd  21823  psdmvr  22073  tx2cn  23514  ustuqtop5  24150  iocopnst  24854  cmetcaulem  25205  dvaddbr  25857  dvmulbr  25858  dvmulbrOLD  25859  tglineeltr  28595  wlkp1lem6  29641  upgr1wlkdlem2  30109  grplsm0l  33359  ressply1invg  33523  poimirlem17  37636  poimirlem20  37639  rngonegmn1l  37940  qsdisjALTV  38611  mplmapghm  42549  naddcnfid1  43360  icccncfext  45888  isubgr3stgrlem7  47976  pgnbgreunbgrlem3  48122  pgnbgreunbgrlem6  48128