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

 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 1261 . . 3 ((𝜓𝜑𝜒) → 𝜃)
323adant1l 1310 . 2 (((𝜏𝜓) ∧ 𝜑𝜒) → 𝜃)
433com12 1261 1 ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  axdc3lem4  9158  modexp  12861  lmmbr2  22865  ax5seglem1  25608  ax5seglem2  25609  nvaddsub4  26896  pl1cn  29329  athgt  33760  ltrncoelN  34447  ltrncoat  34448  trlcoabs  35027  tendoplcl2  35084  tendopltp  35086  dih1dimatlem0  35635  pellex  36417  fourierdlem42  39042
 Copyright terms: Public domain W3C validator