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  6208  zorn2lem6  8128  lemul12b  9613  lt2mul2div  9632  lediv12a  9649  tgcl  16707  neissex  16864  alexsublem  17738  alexsubALTlem4  17744  iscmet3  18719  ablo4  20954  shscli  21896  mdslmd3i  22912  cvmliftmolem2  23813  heibor  26545  ablo4pnp  26570  crngm4  26628  mzpcompact2lem  26829  cvratlem  29610  ps-2  29667  cdlemftr3  30754
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