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

Theorem 3adant2l 1360
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 1288 . . 3 ((𝜓𝜑𝜒) → 𝜃)
323adant1l 1358 . 2 (((𝜏𝜓) ∧ 𝜑𝜒) → 𝜃)
433com12 1288 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:  axdc3lem4  9313  modexp  13039  lmmbr2  23103  ax5seglem1  25853  ax5seglem2  25854  nvaddsub4  27640  pl1cn  30129  athgt  35060  ltrncoelN  35747  ltrncoat  35748  trlcoabs  36326  tendoplcl2  36383  tendopltp  36385  dih1dimatlem0  36934  pellex  37716  fourierdlem42  40684
  Copyright terms: Public domain W3C validator