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  11102  lediv23  11103  divalglem8  15321  isdrngd  18970  deg1tm  24073  ax5seglem1  26003  ax5seglem2  26004  nvaddsub4  27817  nmoub2i  27934  cdleme21at  36114  cdleme42f  36266  trlcoabs2N  36508  tendoplcl2  36564  tendopltp  36566  cdlemk2  36618  cdlemk8  36624  cdlemk9  36625  cdlemk9bN  36626  cdleml8  36769  dihglblem3N  37082  dihglblem3aN  37083  fourierdlem42  40865  lincscm  42725
  Copyright terms: Public domain W3C validator