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

Theorem adantrrr 763
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 474 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 688 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  2ndconst  7435  zorn2lem6  9535  addsrmo  10106  mulsrmo  10107  lemul12b  11092  lt2mul2div  11113  lediv12a  11128  tgcl  20995  neissex  21153  alexsublem  22069  alexsubALTlem4  22075  iscmet3  23311  ablo4  27734  shscli  28506  mdslmd3i  29521  cvmliftmolem2  31592  mblfinlem4  33780  heibor  33951  ablo4pnp  34010  crngm4  34133  cvratlem  35228  ps-2  35285  cdlemftr3  36373  mzpcompact2lem  37834
  Copyright terms: Public domain W3C validator