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  7120  oeoelem  8562  qsdisj  8767  faclbnd4lem4  14261  sumrb  15679  prodrblem2  15897  pwspjmhmmgpd  20237  asclpropd  21806  psdmvr  22056  tx2cn  23497  ustuqtop5  24133  iocopnst  24837  cmetcaulem  25188  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  tglineeltr  28558  wlkp1lem6  29606  upgr1wlkdlem2  30075  grplsm0l  33374  ressply1invg  33538  poimirlem17  37631  poimirlem20  37634  rngonegmn1l  37935  qsdisjALTV  38606  mplmapghm  42544  naddcnfid1  43356  icccncfext  45885  isubgr3stgrlem7  47971  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114