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  7143  oeoelem  8615  qsdisj  8813  faclbnd4lem4  14319  sumrb  15734  prodrblem2  15952  pwspjmhmmgpd  20293  asclpropd  21862  psdmvr  22112  tx2cn  23553  ustuqtop5  24189  iocopnst  24893  cmetcaulem  25245  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  tglineeltr  28615  wlkp1lem6  29663  upgr1wlkdlem2  30132  grplsm0l  33423  ressply1invg  33587  poimirlem17  37666  poimirlem20  37669  rngonegmn1l  37970  qsdisjALTV  38638  mplmapghm  42546  naddcnfid1  43358  icccncfext  45883  isubgr3stgrlem7  47951