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  6850  odi  6851  oelim2  6867  mapxpen  7302  unwdomg  7581  dfac12lem2  8055  infunsdom  8125  fin1a2s  8325  fbasrn  17947  lmmbr  19242  grporcan  21840  unoplin  23454  hmoplin  23476  superpos  23888  subfacp1lem5  24901  itg2addnclem  26294  ftc1anclem6  26323  fdc  26487  ismtyres  26555  isdrngo2  26612  rngohomco  26628  rngoisocnv  26635  frlmup1  27265  stoweidlem27  27790
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