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

Theorem adantrrr 729
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  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
adantrrr  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  ta ) ) )  ->  th )

Proof of Theorem adantrrr
StepHypRef Expression
1 simpl 458 . 2  |-  ( ( ch  /\  ta )  ->  ch )
2 adantr2.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylanr2 657 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  ta ) ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  2ndconst  6840  zorn2lem6  8882  addsrmo  9448  mulsrmo  9449  lemul12b  10413  lt2mul2div  10434  lediv12a  10450  tgcl  19927  neissex  20085  alexsublem  21001  alexsubALTlem4  21007  iscmet3  22205  ablo4  25957  shscli  26912  mdslmd3i  27927  cvmliftmolem2  29957  mblfinlem4  31887  heibor  32060  ablo4pnp  32085  crngm4  32143  cvratlem  32898  ps-2  32955  cdlemftr3  34044  mzpcompact2lem  35505
  Copyright terms: Public domain W3C validator