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

Theorem 3adant3l 1177
 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 488 . 2 ((𝜏𝜒) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1162 1 ((𝜑𝜓 ∧ (𝜏𝜒)) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  wfrlem12  7952  ecopovtrn  8386  rrxmet  24022  nvaddsub4  28450  adjlnop  29879  pl1cn  31323  rrnmet  35286  lflsub  36382  lflmul  36383  cvlatexch3  36653  cdleme5  37555  cdlemeg46rjgN  37837  cdlemg2l  37918  cdlemg10c  37954  tendospcanN  38338  dicvaddcl  38505  dicvscacl  38506  dochexmidlem8  38782  limsupre3lem  42417  fourierdlem42  42834  fourierdlem113  42904  ovnsupge0  43239  ovncvrrp  43246  ovnhoilem2  43284
 Copyright terms: Public domain W3C validator