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

Theorem 3adant2r 1176
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 486 . 2 ((𝜓𝜏) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1161 1 ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ltdiv23  11529  lediv23  11530  divalglem8  15749  isdrngd  19527  deg1tm  24722  ax5seglem1  26725  ax5seglem2  26726  nvaddsub4  28443  nmoub2i  28560  cdleme21at  37569  cdleme42f  37721  trlcoabs2N  37963  tendoplcl2  38019  tendopltp  38021  cdlemk2  38073  cdlemk8  38079  cdlemk9  38080  cdlemk9bN  38081  cdleml8  38224  dihglblem3N  38536  dihglblem3aN  38537  fourierdlem42  42717  lincscm  44765  itsclc0yqsol  45104
  Copyright terms: Public domain W3C validator