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  6870  zorn2lem6  8879  addsrmo  9448  mulsrmo  9449  lemul12b  10400  lt2mul2div  10422  lediv12a  10439  tgcl  19337  neissex  19494  alexsublem  20410  alexsubALTlem4  20416  iscmet3  21598  ablo4  25154  shscli  26100  mdslmd3i  27116  cvmliftmolem2  28593  mblfinlem4  30022  heibor  30285  ablo4pnp  30310  crngm4  30368  mzpcompact2lem  30652  cvratlem  34847  ps-2  34904  cdlemftr3  35993
  Copyright terms: Public domain W3C validator