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

Theorem adantrrr 756
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 471 . 2 ((𝜒𝜏) → 𝜒)
2 adantr2.1 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
31, 2sylanr2 682 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜏))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  2ndconst  7126  zorn2lem6  9179  addsrmo  9746  mulsrmo  9747  lemul12b  10725  lt2mul2div  10746  lediv12a  10761  tgcl  20522  neissex  20679  alexsublem  21596  alexsubALTlem4  21602  iscmet3  22813  ablo4  26553  shscli  27362  mdslmd3i  28377  cvmliftmolem2  30320  mblfinlem4  32418  heibor  32589  ablo4pnp  32648  crngm4  32771  cvratlem  33524  ps-2  33581  cdlemftr3  34670  mzpcompact2lem  36131
  Copyright terms: Public domain W3C validator