Theorem mpidan 685

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 683	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 206  df-an 396

This theorem is referenced by:  funopsn  7002  oeoelem  8391  qsdisj  8541  faclbnd4lem4  13938  sumrb  15353  prodrblem2  15569  asclpropd  21011  tx2cn  22669  ustuqtop5  23305  iocopnst  24009  cmetcaulem  24357  dvaddbr  25007  dvmulbr  25008  tglineeltr  26896  wlkp1lem6  27948  upgr1wlkdlem2  28411  grplsm0l  31493  poimirlem17  35721  poimirlem20  35724  rngonegmn1l  36026  qsdisjALTV  36655  pwspjmhmmgpd  40192  icccncfext  43318  isomuspgrlem2c  45170