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

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

StepHypRef Expression
1 simpl 486 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 682 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  zorn2lem6  9916  addsrmo  10488  mulsrmo  10489  lemul12b  11490  lt2mul2div  11511  lediv12a  11526  tgcl  21577  neissex  21735  alexsublem  22652  alexsubALTlem4  22658  iscmet3  23900  ablo4  28336  shscli  29103  mdslmd3i  30118  cvmliftmolem2  32637  mblfinlem4  35090  heibor  35252  ablo4pnp  35311  crngm4  35434  cvratlem  36710  ps-2  36767  cdlemftr3  37854  mzpcompact2lem  39679
 Copyright terms: Public domain W3C validator