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

Theorem 3adant2l 1178
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 485 . 2 ((𝜏𝜓) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1164 1 ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  axdc3lem4  10450  modexp  14203  lmmbr2  24783  ax5seglem1  28224  ax5seglem2  28225  nvaddsub4  29948  pl1cn  33004  athgt  38413  ltrncoelN  39100  ltrncoat  39101  trlcoabs  39678  tendoplcl2  39735  tendopltp  39737  dih1dimatlem0  40285  pellex  41655  fourierdlem42  44944
  Copyright terms: Public domain W3C validator