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

Theorem adantrlr 723
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 482 . 2 ((𝜓𝜏) → 𝜓)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr1 682 1 ((𝜑 ∧ ((𝜓𝜏) ∧ 𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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
This theorem is referenced by:  smoord  8405  addsrmo  11113  mulsrmo  11114  lediv12a  12161  nrmmetd  24587  pntrmax  27608  ablo4  30569  mdslmd3i  32351  atom1d  32372  fsumiunle  32831  esumiun  34095  poimirlem28  37655  fdc  37752  incsequz  37755  crngm4  38010  ps-2  39480  aacllem  49320
  Copyright terms: Public domain W3C validator