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  7629  addsrmo  10084  mulsrmo  10085  lediv12a  11106  nrmmetd  22578  pntrmax  25450  ablo4  27711  mdslmd3i  29498  atom1d  29519  fsumiunle  29882  esumiun  30463  poimirlem28  33748  fdc  33852  incsequz  33855  crngm4  34113  ps-2  35265  aacllem  43058
  Copyright terms: Public domain W3C validator