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  7093  oeoelem  8526  qsdisj  8731  faclbnd4lem4  14219  sumrb  15636  prodrblem2  15854  pwspjmhmmgpd  20263  asclpropd  21853  psdmvr  22112  tx2cn  23554  ustuqtop5  24189  iocopnst  24893  cmetcaulem  25244  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  tglineeltr  28703  wlkp1lem6  29750  upgr1wlkdlem2  30221  grplsm0l  33484  ressply1invg  33650  mplvrpmmhm  33711  mplvrpmrhm  33712  poimirlem17  37838  poimirlem20  37841  rngonegmn1l  38142  qsdisjALTV  38872  mplmapghm  42807  naddcnfid1  43609  icccncfext  46131  isubgr3stgrlem7  48218  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370