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

Theorem 3adantr1 1212
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 1052 . 2 ((𝜏𝜓𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 489 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3ad2antr3  1220  3adant3r1  1265  swopo  4958  omeulem1  7526  divmuldiv  10576  imasmnd2  17098  imasgrp2  17301  srgbinomlem2  18312  imasring  18390  abvdiv  18608  mdetunilem9  20192  lly1stc  21056  icccvx  22504  dchrpt  24736  dipsubdir  26880  poimirlem4  32366  fdc  32494  unichnidl  32783  dmncan1  32828  pexmidlem6N  34062  erngdvlem3  35079  erngdvlem3-rN  35087  dvalveclem  35115  dvhvaddass  35187  dvhlveclem  35198  issmflem  39396
  Copyright terms: Public domain W3C validator