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

Theorem 3adant3l 1180
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
3adant3l ((𝜑𝜓 ∧ (𝜏𝜒)) → 𝜃)

Proof of Theorem 3adant3l
StepHypRef Expression
1 simpr 485 . 2 ((𝜏𝜒) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1165 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:  wfrlem12OLD  8265  ecopovtrn  8758  rrxmet  24770  nvaddsub4  29546  adjlnop  30975  pl1cn  32476  rrnmet  36278  lflsub  37519  lflmul  37520  cvlatexch3  37790  cdleme5  38693  cdlemeg46rjgN  38975  cdlemg2l  39056  cdlemg10c  39092  tendospcanN  39476  dicvaddcl  39643  dicvscacl  39644  dochexmidlem8  39920  limsupre3lem  43944  fourierdlem42  44361  fourierdlem113  44431  ovnsupge0  44769  ovncvrrp  44776  ovnhoilem2  44814
  Copyright terms: Public domain W3C validator