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

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

Proof of Theorem 3adantr2
StepHypRef Expression
1 3simpb 1057 . 2 ((𝜓𝜏𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 491 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  3adant3r2  1272  po3nr  5019  funcnvqp  5920  sornom  9059  axdclem2  9302  fzadd2  12334  issubc3  16449  funcestrcsetclem9  16728  funcsetcestrclem9  16743  pgpfi  17960  imasring  18559  prdslmodd  18909  icoopnst  22678  iocopnst  22679  axcontlem4  25781  nvmdi  27391  mdsl3  29063  elicc3  32006  iscringd  33468  erngdvlem3  35797  erngdvlem3-rN  35805  dvalveclem  35833  dvhlveclem  35916  dvmptfprodlem  39496  smflimlem4  40319  funcringcsetcALTV2lem9  41362  funcringcsetclem9ALTV  41385
  Copyright terms: Public domain W3C validator