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

Theorem 3adant2r 1171
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 483 . 2 ((𝜓𝜏) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1156 1 ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ltdiv23  11520  lediv23  11521  divalglem8  15741  isdrngd  19458  deg1tm  24641  ax5seglem1  26642  ax5seglem2  26643  nvaddsub4  28362  nmoub2i  28479  cdleme21at  37346  cdleme42f  37498  trlcoabs2N  37740  tendoplcl2  37796  tendopltp  37798  cdlemk2  37850  cdlemk8  37856  cdlemk9  37857  cdlemk9bN  37858  cdleml8  38001  dihglblem3N  38313  dihglblem3aN  38314  fourierdlem42  42315  lincscm  44383  itsclc0yqsol  44649
  Copyright terms: Public domain W3C validator