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  7168  oeoelem  8636  qsdisj  8834  faclbnd4lem4  14335  sumrb  15749  prodrblem2  15967  pwspjmhmmgpd  20325  asclpropd  21917  psdmvr  22173  tx2cn  23618  ustuqtop5  24254  iocopnst  24970  cmetcaulem  25322  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  tglineeltr  28639  wlkp1lem6  29696  upgr1wlkdlem2  30165  grplsm0l  33431  ressply1invg  33594  poimirlem17  37644  poimirlem20  37647  rngonegmn1l  37948  qsdisjALTV  38616  mplmapghm  42566  naddcnfid1  43380  icccncfext  45902  isubgr3stgrlem7  47939