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

Theorem adantrrr 724
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 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