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

Theorem 3adant3l 1193
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 471 . 2 ((𝜏𝜒) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1169 1 ((𝜑𝜓 ∧ (𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  wfrlem12  7583  ecopovtrn  8007  rrxmet  23410  nvaddsub4  27852  adjlnop  29285  pl1cn  30341  rrnmet  33960  lflsub  34876  lflmul  34877  cvlatexch3  35147  cdleme5  36050  cdlemeg46rjgN  36332  cdlemg2l  36413  cdlemg10c  36449  tendospcanN  36833  dicvaddcl  37000  dicvscacl  37001  dochexmidlem8  37277  limsupre3lem  40479  fourierdlem42  40880  fourierdlem113  40950  ovnsupge0  41288  ovncvrrp  41295  ovnhoilem2  41333
  Copyright terms: Public domain W3C validator