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

Theorem adantrrr 705
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 443 . 2  |-  ( ( ch  /\  ta )  ->  ch )
2 adantr2.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylanr2 634 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  ta ) ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  2ndconst  6224  zorn2lem6  8144  lemul12b  9629  lt2mul2div  9648  lediv12a  9665  tgcl  16723  neissex  16880  alexsublem  17754  alexsubALTlem4  17760  iscmet3  18735  ablo4  20970  shscli  21912  mdslmd3i  22928  cvmliftmolem2  23828  itg2addnclem  25003  heibor  26648  ablo4pnp  26673  crngm4  26731  mzpcompact2lem  26932  cvratlem  30232  ps-2  30289  cdlemftr3  31376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator