Theorem mpidan 688

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 686	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  7182  oeoelem  8654  qsdisj  8852  faclbnd4lem4  14345  sumrb  15761  prodrblem2  15979  pwspjmhmmgpd  20351  asclpropd  21940  tx2cn  23639  ustuqtop5  24275  iocopnst  24989  cmetcaulem  25341  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  tglineeltr  28657  wlkp1lem6  29714  upgr1wlkdlem2  30178  grplsm0l  33396  ressply1invg  33559  poimirlem17  37597  poimirlem20  37600  rngonegmn1l  37901  qsdisjALTV  38571  mplmapghm  42511  naddcnfid1  43329  icccncfext  45808