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

Theorem adantlrl 719
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 461 . 2  |-  ( ( ta  /\  ps )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 651 1  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  omlimcl  7038  odi  7039  oelim2  7055  mapxpen  7498  unwdomg  7820  dfac12lem2  8334  infunsdom  8404  fin1a2s  8604  frlmup1  18248  fbasrn  19479  lmmbr  20791  grporcan  23730  unoplin  25346  hmoplin  25368  superpos  25780  subfacp1lem5  27094  itg2addnclem  28469  ftc1anclem6  28498  fdc  28667  ismtyres  28733  isdrngo2  28790  rngohomco  28806  rngoisocnv  28813  stoweidlem27  29848
  Copyright terms: Public domain W3C validator