Theorem mpidan 690

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 688	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  7095  oeoelem  8527  qsdisj  8734  faclbnd4lem4  14249  sumrb  15666  prodrblem2  15887  pwspjmhmmgpd  20298  asclpropd  21887  psdmvr  22145  tx2cn  23585  ustuqtop5  24220  iocopnst  24917  cmetcaulem  25265  dvaddbr  25915  dvmulbr  25916  tglineeltr  28713  wlkp1lem6  29760  upgr1wlkdlem2  30231  grplsm0l  33478  ressply1invg  33644  mplvrpmmhm  33705  mplvrpmrhm  33706  poimirlem17  37972  poimirlem20  37975  rngonegmn1l  38276  qsdisjALTV  39034  mplmapghm  43011  naddcnfid1  43813  icccncfext  46333  isubgr3stgrlem7  48460  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612