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

Theorem 3adant2l 1179
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
Hypothesis
Ref Expression
ad4ant3.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant2l ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant2l
StepHypRef Expression
1 simpr 486 . 2 ((𝜏𝜓) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1165 1 ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  axdc3lem4  10448  modexp  14201  lmmbr2  24776  ax5seglem1  28186  ax5seglem2  28187  nvaddsub4  29910  pl1cn  32935  athgt  38327  ltrncoelN  39014  ltrncoat  39015  trlcoabs  39592  tendoplcl2  39649  tendopltp  39651  dih1dimatlem0  40199  pellex  41573  fourierdlem42  44865
  Copyright terms: Public domain W3C validator