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

Theorem 3adant1l 1177
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 486 . 2 ((𝜏𝜑) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1164 1 (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  ad5ant245  1362  cfsmolem  10214  axdc3lem4  10397  issubmnd  18591  maducoeval2  22012  cramerlem3  22061  restnlly  22856  efgh  25920  hasheuni  32748  matunitlindflem1  36124  pellex  41205  mendlmod  41567  disjf1o  43502  ssfiunibd  43634  mullimc  43947  mullimcf  43954  limclner  43982  limsupresxr  44097  liminfresxr  44098  sge0lefi  44729  isomenndlem  44861  hoicvr  44879  ovncvrrp  44895
  Copyright terms: Public domain W3C validator