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

Theorem 3adantr1 1166
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3adantr1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)

Proof of Theorem 3adantr1
StepHypRef Expression
1 3simpc 1147 . 2 ((𝜏𝜓𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 595 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:  3adant3r1  1179  3ad2antr3  1187  swopo  5471  omeulem1  8204  divmuldiv  11338  imasmnd2  17948  imasgrp2  18214  srgbinomlem2  19291  imasring  19372  abvdiv  19608  mdetunilem9  21232  lly1stc  22108  icccvx  23562  dchrpt  25858  dipsubdir  28638  poimirlem4  35010  fdc  35132  unichnidl  35418  dmncan1  35463  pexmidlem6N  37220  erngdvlem3  38235  erngdvlem3-rN  38243  dvalveclem  38270  dvhvaddass  38342  dvhlveclem  38353  issmflem  43292  prproropf1olem3  43953
  Copyright terms: Public domain W3C validator