Theorem mpidan 686

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 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpidan.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpdan 684	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  funopsn  7020  oeoelem  8429  qsdisj  8583  faclbnd4lem4  14010  sumrb  15425  prodrblem2  15641  asclpropd  21101  tx2cn  22761  ustuqtop5  23397  iocopnst  24103  cmetcaulem  24452  dvaddbr  25102  dvmulbr  25103  tglineeltr  26992  wlkp1lem6  28046  upgr1wlkdlem2  28510  grplsm0l  31591  poimirlem17  35794  poimirlem20  35797  rngonegmn1l  36099  qsdisjALTV  36728  pwspjmhmmgpd  40267  icccncfext  43428  isomuspgrlem2c  45282