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  7228  odi  7229  oelim2  7245  mapxpen  7684  unwdomg  8011  dfac12lem2  8525  infunsdom  8595  fin1a2s  8795  frlmup1  18639  fbasrn  20212  lmmbr  21524  grporcan  24996  unoplin  26612  hmoplin  26634  superpos  27046  subfacp1lem5  28379  itg2addnclem  29919  ftc1anclem6  29948  fdc  30068  ismtyres  30134  isdrngo2  30191  rngohomco  30207  rngoisocnv  30214  stoweidlem27  31554  fourierdlem97  31731
  Copyright terms: Public domain W3C validator