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

Theorem 3adantr2 1171
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 1150 . 2 ((𝜓𝜏𝜒) → (𝜓𝜒))
2 3adantr.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylan2 593 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3adant3r2  1184  po3nr  5607  funcnvqp  6630  sornom  10317  axdclem2  10560  fzadd2  13599  issubc3  17894  funcestrcsetclem9  18193  funcsetcestrclem9  18208  pgpfi  19623  imasrng  20174  imasring  20327  prdslmodd  20967  icoopnst  24969  iocopnst  24970  axcontlem4  28982  nvmdi  30667  mdsl3  32335  elicc3  36318  iscringd  38005  erngdvlem3  40992  erngdvlem3-rN  41000  dvalveclem  41027  dvhlveclem  41110  dvmptfprodlem  45959  smflimlem4  46789  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237
  Copyright terms: Public domain W3C validator