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 594 1 ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3adant3r2  1184  po3nr  5564  funcnvqp  6569  sornom  10221  axdclem2  10464  fzadd2  13485  issubc3  17743  funcestrcsetclem9  18044  funcsetcestrclem9  18059  pgpfi  19395  imasring  20053  prdslmodd  20474  icoopnst  24325  iocopnst  24326  axcontlem4  27965  nvmdi  29639  mdsl3  31307  elicc3  34842  iscringd  36507  erngdvlem3  39503  erngdvlem3-rN  39511  dvalveclem  39538  dvhlveclem  39621  dvmptfprodlem  44275  smflimlem4  45105  funcringcsetcALTV2lem9  46432  funcringcsetclem9ALTV  46455
  Copyright terms: Public domain W3C validator