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  7090  oeoelem  8522  qsdisj  8727  faclbnd4lem4  14210  sumrb  15627  prodrblem2  15845  pwspjmhmmgpd  20254  asclpropd  21844  psdmvr  22103  tx2cn  23545  ustuqtop5  24180  iocopnst  24884  cmetcaulem  25235  dvaddbr  25887  dvmulbr  25888  dvmulbrOLD  25889  tglineeltr  28629  wlkp1lem6  29676  upgr1wlkdlem2  30147  grplsm0l  33412  ressply1invg  33578  mplvrpmmhm  33639  mplvrpmrhm  33640  poimirlem17  37750  poimirlem20  37753  rngonegmn1l  38054  qsdisjALTV  38784  mplmapghm  42722  naddcnfid1  43524  icccncfext  46047  isubgr3stgrlem7  48134  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem6  48286