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

Theorem adantrrr 725
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 482 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 683 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  zorn2lem6  10541  addsrmo  11113  mulsrmo  11114  lemul12b  12124  lt2mul2div  12146  lediv12a  12161  tgcl  22976  neissex  23135  alexsublem  24052  alexsubALTlem4  24058  iscmet3  25327  mulsuniflem  28175  ablo4  30569  shscli  31336  mdslmd3i  32351  brab2d  32619  cvmliftmolem2  35287  mblfinlem4  37667  heibor  37828  ablo4pnp  37887  crngm4  38010  cvratlem  39423  ps-2  39480  cdlemftr3  40567  mzpcompact2lem  42762
  Copyright terms: Public domain W3C validator