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

Theorem adantrrr 707
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 470 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 665 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  2ndconst  7510  zorn2lem6  9618  addsrmo  10189  mulsrmo  10190  lemul12b  11175  lt2mul2div  11196  lediv12a  11211  tgcl  21008  neissex  21166  alexsublem  22082  alexsubALTlem4  22088  iscmet3  23325  ablo4  27756  shscli  28527  mdslmd3i  29542  cvmliftmolem2  31609  mblfinlem4  33781  heibor  33950  ablo4pnp  34009  crngm4  34132  cvratlem  35220  ps-2  35277  cdlemftr3  36364  mzpcompact2lem  37834
  Copyright terms: Public domain W3C validator