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

Theorem 3adant1l 1174
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 483 . 2 ((𝜏𝜑) → 𝜑)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an1 1161 1 (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  ad5ant245  1359  cfsmolem  10267  axdc3lem4  10450  issubmnd  18686  mhmima  18742  rhmimasubrng  20454  maducoeval2  22362  cramerlem3  22411  restnlly  23206  efgh  26286  hasheuni  33381  matunitlindflem1  36787  pellex  41875  mendlmod  42237  disjf1o  44188  ssfiunibd  44317  mullimc  44630  mullimcf  44637  limclner  44665  limsupresxr  44780  liminfresxr  44781  sge0lefi  45412  isomenndlem  45544  hoicvr  45562  ovncvrrp  45578
  Copyright terms: Public domain W3C validator