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  7123  oeoelem  8565  qsdisj  8770  faclbnd4lem4  14268  sumrb  15686  prodrblem2  15904  pwspjmhmmgpd  20244  asclpropd  21813  psdmvr  22063  tx2cn  23504  ustuqtop5  24140  iocopnst  24844  cmetcaulem  25195  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  tglineeltr  28565  wlkp1lem6  29613  upgr1wlkdlem2  30082  grplsm0l  33381  ressply1invg  33545  poimirlem17  37638  poimirlem20  37641  rngonegmn1l  37942  qsdisjALTV  38613  mplmapghm  42551  naddcnfid1  43363  icccncfext  45892  isubgr3stgrlem7  47975  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118