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

Theorem adantlrl 701
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 448 . 2  |-  ( ( ta  /\  ps )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 633 1  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  omlimcl  6807  odi  6808  oelim2  6824  mapxpen  7259  unwdomg  7536  dfac12lem2  8008  infunsdom  8078  fin1a2s  8278  fbasrn  17899  lmmbr  19194  grporcan  21792  unoplin  23406  hmoplin  23428  superpos  23840  subfacp1lem5  24853  itg2addnclem  26197  fdc  26381  ismtyres  26449  isdrngo2  26506  rngohomco  26522  rngoisocnv  26529  frlmup1  27160  stoweidlem27  27685
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 178  df-an 361
  Copyright terms: Public domain W3C validator