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

Theorem adantrlr 761
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantr2.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
adantrlr ((𝜑 ∧ ((𝜓𝜏) ∧ 𝜒)) → 𝜃)

Proof of Theorem adantrlr
StepHypRef Expression
1 simpl 474 . 2 ((𝜓𝜏) → 𝜓)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr1 687 1 ((𝜑 ∧ ((𝜓𝜏) ∧ 𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  smoord  7632  addsrmo  10106  mulsrmo  10107  lediv12a  11128  nrmmetd  22600  pntrmax  25473  ablo4  27734  mdslmd3i  29521  atom1d  29542  fsumiunle  29905  esumiun  30486  poimirlem28  33768  fdc  33872  incsequz  33875  crngm4  34133  ps-2  35285  aacllem  43078
  Copyright terms: Public domain W3C validator