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

Theorem 3adantr1 1175
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 492 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  3adant3r1  1198  3ad2antr3  1206  swopo  5195  omeulem1  7829  divmuldiv  10915  imasmnd2  17526  imasgrp2  17729  srgbinomlem2  18739  imasring  18817  abvdiv  19037  mdetunilem9  20626  lly1stc  21499  icccvx  22948  dchrpt  25189  dipsubdir  28010  poimirlem4  33724  fdc  33852  unichnidl  34141  dmncan1  34186  pexmidlem6N  35762  erngdvlem3  36778  erngdvlem3-rN  36786  dvalveclem  36814  dvhvaddass  36886  dvhlveclem  36897  issmflem  41440
  Copyright terms: Public domain W3C validator