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

Theorem adantlrl 700
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 447 . 2  |-  ( ( ta  /\  ps )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 632 1  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  omlimcl  6660  odi  6661  oelim2  6677  mapxpen  7112  unwdomg  7385  dfac12lem2  7857  infunsdom  7927  fin1a2s  8127  fbasrn  17675  lmmbr  18782  grporcan  20994  unoplin  22608  hmoplin  22630  superpos  23042  subfacp1lem5  24119  itg2addnclem  25492  fdc  25779  ismtyres  25855  isdrngo2  25912  rngohomco  25928  rngoisocnv  25935  frlmup1  26573
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 177  df-an 360
  Copyright terms: Public domain W3C validator