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

Theorem adantrlr 721
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 483 . 2 ((𝜓𝜏) → 𝜓)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr1 680 1 ((𝜑 ∧ ((𝜓𝜏) ∧ 𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  smoord  8311  addsrmo  11009  mulsrmo  11010  lediv12a  12048  nrmmetd  23930  pntrmax  26912  ablo4  29492  mdslmd3i  31274  atom1d  31295  fsumiunle  31725  esumiun  32693  poimirlem28  36106  fdc  36204  incsequz  36207  crngm4  36462  ps-2  37941  aacllem  47238
  Copyright terms: Public domain W3C validator