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

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

Proof of Theorem 3adant1l
StepHypRef Expression
1 simpr 488 . 2 ((𝜏𝜑) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1160 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:  ad5ant245  1358  cfsmolem  9699  axdc3lem4  9882  issubmnd  17950  maducoeval2  21286  cramerlem3  21335  restnlly  22128  efgh  25177  hasheuni  31520  matunitlindflem1  35204  pellex  39947  mendlmod  40308  disjf1o  41988  ssfiunibd  42109  mullimc  42426  mullimcf  42433  limclner  42461  limsupresxr  42576  liminfresxr  42577  sge0lefi  43205  isomenndlem  43337  hoicvr  43355  ovncvrrp  43371
 Copyright terms: Public domain W3C validator