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

Theorem adantlrl 717
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 459 . 2  |-  ( ( ta  /\  ps )  ->  ps )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl2 649 1  |-  ( ( ( ph  /\  ( ta  /\  ps ) )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  omlimcl  7219  odi  7220  oelim2  7236  mapxpen  7676  unwdomg  8002  dfac12lem2  8515  infunsdom  8585  fin1a2s  8785  frlmup1  19003  fbasrn  20554  lmmbr  21866  grporcan  25424  unoplin  27040  hmoplin  27062  superpos  27474  subfacp1lem5  28895  itg2addnclem  30309  ftc1anclem6  30338  fdc  30481  ismtyres  30547  isdrngo2  30604  rngohomco  30620  rngoisocnv  30627  dvdsn1add  31978  dvnprodlem1  31985  stoweidlem27  32051  fourierdlem97  32228
  Copyright terms: Public domain W3C validator