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  6788  odi  6789  oelim2  6805  mapxpen  7240  unwdomg  7516  dfac12lem2  7988  infunsdom  8058  fin1a2s  8258  fbasrn  17877  lmmbr  19172  grporcan  21770  unoplin  23384  hmoplin  23406  superpos  23818  subfacp1lem5  24831  itg2addnclem  26163  fdc  26347  ismtyres  26415  isdrngo2  26472  rngohomco  26488  rngoisocnv  26495  frlmup1  27126  stoweidlem27  27651
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