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

Theorem 3adant2r 1192
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 474 . 2 ((𝜓𝜏) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1168 1 ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  ltdiv23  11127  lediv23  11128  divalglem8  15346  isdrngd  18995  deg1tm  24098  ax5seglem1  26029  ax5seglem2  26030  nvaddsub4  27843  nmoub2i  27960  cdleme21at  36137  cdleme42f  36289  trlcoabs2N  36531  tendoplcl2  36587  tendopltp  36589  cdlemk2  36641  cdlemk8  36647  cdlemk9  36648  cdlemk9bN  36649  cdleml8  36792  dihglblem3N  37105  dihglblem3aN  37106  fourierdlem42  40888  lincscm  42748
  Copyright terms: Public domain W3C validator