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

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

Proof of Theorem 3adant2l
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213com12 1266 . . 3 ((𝜓𝜑𝜒) → 𝜃)
323adant1l 1315 . 2 (((𝜏𝜓) ∧ 𝜑𝜒) → 𝜃)
433com12 1266 1 ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  axdc3lem4  9220  modexp  12936  lmmbr2  22960  ax5seglem1  25703  ax5seglem2  25704  nvaddsub4  27352  pl1cn  29775  athgt  34208  ltrncoelN  34895  ltrncoat  34896  trlcoabs  35475  tendoplcl2  35532  tendopltp  35534  dih1dimatlem0  36083  pellex  36865  fourierdlem42  39660
  Copyright terms: Public domain W3C validator