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

Theorem 3adantr2 1172
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 1141 . 2 ((𝜓𝜏𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 586 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  3adant3r2  1191  po3nr  5290  funcnvqp  6200  sornom  9436  axdclem2  9679  fzadd2  12698  issubc3  16905  funcestrcsetclem9  17185  funcsetcestrclem9  17200  pgpfi  18415  imasring  19017  prdslmodd  19375  icoopnst  23157  iocopnst  23158  axcontlem4  26333  nvmdi  28092  mdsl3  29764  elicc3  32908  iscringd  34430  erngdvlem3  37153  erngdvlem3-rN  37161  dvalveclem  37188  dvhlveclem  37271  dvmptfprodlem  41101  smflimlem4  41923  funcringcsetcALTV2lem9  43073  funcringcsetclem9ALTV  43096
  Copyright terms: Public domain W3C validator