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

Theorem adantrrr 704
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
adantrrr ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)

Proof of Theorem adantrrr
StepHypRef Expression
1 simpl 468 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 662 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  2ndconst  7417  zorn2lem6  9525  addsrmo  10096  mulsrmo  10097  lemul12b  11082  lt2mul2div  11103  lediv12a  11118  tgcl  20994  neissex  21152  alexsublem  22068  alexsubALTlem4  22074  iscmet3  23310  ablo4  27744  shscli  28516  mdslmd3i  29531  cvmliftmolem2  31602  mblfinlem4  33782  heibor  33952  ablo4pnp  34011  crngm4  34134  cvratlem  35229  ps-2  35286  cdlemftr3  36374  mzpcompact2lem  37840
  Copyright terms: Public domain W3C validator