Theorem adantlrr 757

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
adantlrr	|- ( ( ( ph /\ ( ps /\ ta ) ) /\ ch ) -> th )

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ps /\ ta ) -> ps )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl2 683	1 |- ( ( ( ph /\ ( ps /\ ta ) ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  disjxiun  4649  oelim  7614  odi  7659  marypha1lem  8339  dfac12lem2  8966  infunsdom  9036  isf34lem4  9199  distrlem1pr  9847  lcmgcdlem  15319  lcmdvds  15321  drsdirfi  16938  isacs3lem  17166  conjnmzb  17695  psgndif  19948  frlmsslsp  20135  metss2lem  22316  nghmcn  22549  bndth  22757  itg2monolem1  23517  dvmptfsum  23738  ply1divex  23896  itgulm  24162  rpvmasumlem  25176  dchrmusum2  25183  dchrisum0lem2  25207  dchrisum0lem3  25208  mulog2sumlem2  25224  pntibndlem3  25281  wwlksubclwwlks  26925  blocni  27660  superpos  29213  chirredlem2  29250  eulerpartlemgvv  30438  ballotlemfc0  30554  ballotlemfcc  30555  bj-finsumval0  33147  fin2solem  33395  matunitlindflem1  33405  poimirlem28  33437  heicant  33444  ftc1anclem6  33490  ftc1anc  33493  fdc  33541  incsequz  33544  ismtyres  33607  isdrngo2  33757  rngohomco  33773  keridl  33831  linepsubN  35038  pmapsub  35054  mzpcompact2lem  37314  pellex  37399  monotuz  37506  unxpwdom3  37665  dssmapnvod  38314  radcnvrat  38513  fprodexp  39826  fprodabs2  39827  climxrrelem  39981  dvnprodlem1  40161  stoweidlem34  40251  fourierdlem42  40366  elaa2  40451  sge0iunmptlemfi  40630  aacllem  42547