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 484 . 2 ((𝜏𝜑) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1164 1 (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  ad5ant245  1363  cfsmolem  10310  axdc3lem4  10493  issubmnd  18774  mhmima  18838  rhmimasubrng  20566  maducoeval2  22646  cramerlem3  22695  restnlly  23490  efgh  26583  hasheuni  34086  matunitlindflem1  37623  pellex  42846  mendlmod  43201  disjf1o  45196  ssfiunibd  45321  mullimc  45631  mullimcf  45638  limclner  45666  limsupresxr  45781  liminfresxr  45782  sge0lefi  46413  isomenndlem  46545  hoicvr  46563  ovncvrrp  46579
  Copyright terms: Public domain W3C validator