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

Theorem adantlrl 702
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
adantlrl  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )

Proof of Theorem adantlrl
StepHypRef Expression
1 simpr 449 . 2  |-  ( ( ta  /\  ps )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 634 1  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  omlimcl  6857  odi  6858  oelim2  6874  mapxpen  7309  unwdomg  7588  dfac12lem2  8062  infunsdom  8132  fin1a2s  8332  fbasrn  17954  lmmbr  19249  grporcan  21847  unoplin  23461  hmoplin  23483  superpos  23895  subfacp1lem5  24905  itg2addnclem  26298  ftc1anclem6  26327  fdc  26491  ismtyres  26559  isdrngo2  26616  rngohomco  26632  rngoisocnv  26639  frlmup1  27339  stoweidlem27  27864
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 179  df-an 362
  Copyright terms: Public domain W3C validator