MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3adant2r Structured version   Visualization version   GIF version

Theorem 3adant2r 1184
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
Hypothesis
Ref Expression
ad4ant3.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant2r ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant2r
StepHypRef Expression
1 simpl 476 . 2 ((𝜓𝜏) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1164 1 ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  ltdiv23  11268  lediv23  11269  divalglem8  15530  isdrngd  19164  deg1tm  24315  ax5seglem1  26277  ax5seglem2  26278  nvaddsub4  28098  nmoub2i  28215  cdleme21at  36476  cdleme42f  36628  trlcoabs2N  36870  tendoplcl2  36926  tendopltp  36928  cdlemk2  36980  cdlemk8  36986  cdlemk9  36987  cdlemk9bN  36988  cdleml8  37131  dihglblem3N  37443  dihglblem3aN  37444  fourierdlem42  41285  lincscm  43226  itsclc0yqsol  43492
  Copyright terms: Public domain W3C validator