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

Theorem adantrlr 705
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 470 . 2 ((𝜓𝜏) → 𝜓)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr1 664 1 ((𝜑 ∧ ((𝜓𝜏) ∧ 𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  smoord  7692  addsrmo  10173  mulsrmo  10174  lediv12a  11195  nrmmetd  22586  pntrmax  25461  ablo4  27727  mdslmd3i  29513  atom1d  29534  fsumiunle  29896  esumiun  30475  poimirlem28  33744  fdc  33846  incsequz  33849  crngm4  34107  ps-2  35252  aacllem  43112
  Copyright terms: Public domain W3C validator