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

Theorem adantrrr 724
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 457 . 2  |-  ( ( ch  /\  ta )  ->  ch )
2 adantr2.1 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
31, 2sylanr2 653 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  ta ) ) )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  2ndconst  6662  zorn2lem6  8670  lemul12b  10186  lt2mul2div  10208  lediv12a  10225  tgcl  18574  neissex  18731  alexsublem  19616  alexsubALTlem4  19622  iscmet3  20804  ablo4  23774  shscli  24720  mdslmd3i  25736  cvmliftmolem2  27171  mblfinlem4  28431  heibor  28720  ablo4pnp  28745  crngm4  28803  mzpcompact2lem  29088  cvratlem  33065  ps-2  33122  cdlemftr3  34209
  Copyright terms: Public domain W3C validator