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

Theorem 3adantr1 1169
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 1150 . 2 ((𝜏𝜓𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 593 1 ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  3adant3r1  1182  3ad2antr3  1190  swopo  5554  omeulem1  8525  divmuldiv  11851  imasmnd2  18585  imasgrp2  18853  srgbinomlem2  19944  imasring  20030  abvdiv  20281  mdetunilem9  21953  lly1stc  22831  icccvx  24297  dchrpt  26599  dipsubdir  29676  poimirlem4  36049  fdc  36171  unichnidl  36457  dmncan1  36502  pexmidlem6N  38405  erngdvlem3  39420  erngdvlem3-rN  39428  dvalveclem  39455  dvhvaddass  39527  dvhlveclem  39538  issmflem  44900  prproropf1olem3  45629
  Copyright terms: Public domain W3C validator