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

Theorem 3adant2l 1187
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 479 . 2 ((𝜏𝜓) → 𝜓)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an2 1167 1 ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  axdc3lem4  9459  modexp  13185  lmmbr2  23249  ax5seglem1  25999  ax5seglem2  26000  nvaddsub4  27813  pl1cn  30302  athgt  35237  ltrncoelN  35924  ltrncoat  35925  trlcoabs  36503  tendoplcl2  36560  tendopltp  36562  dih1dimatlem0  37111  pellex  37893  fourierdlem42  40861
  Copyright terms: Public domain W3C validator