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

Theorem 3adant1l 1358
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant1l (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)

Proof of Theorem 3adant1l
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213expb 1285 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32adantll 750 . 2 (((𝜏𝜑) ∧ (𝜓𝜒)) → 𝜃)
433impb 1279 1 (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  3adant2l  1360  3adant3l  1362  cfsmolem  9130  axdc3lem4  9313  issubmnd  17365  maducoeval2  20494  cramerlem3  20543  restnlly  21333  efgh  24332  funvtxdm2valOLD  25940  funiedgdm2valOLD  25941  hasheuni  30275  matunitlindflem1  33535  pellex  37716  mendlmod  38080  disjf1o  39692  ssfiunibd  39837  mullimc  40166  mullimcf  40173  limclner  40201  limsupresxr  40316  liminfresxr  40317  sge0lefi  40933  isomenndlem  41065  hoicvr  41083  ovncvrrp  41099
  Copyright terms: Public domain W3C validator