Theorem ad2ant2rl 785

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad2ant2rl	|- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )

Proof of Theorem ad2ant2rl

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrl 752	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantlr 751	1 |- ( ( ( ph /\ th ) /\ ( ta /\ ps ) ) -> ch )

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:  omwordri  7652  omxpenlem  8061  infxpabs  9034  domfin4  9133  isf32lem7  9181  ordpipq  9764  muladd  10462  lemul12b  10880  mulge0b  10893  qaddcl  11804  iooshf  12252  elfzomelpfzo  12572  expnegz  12894  bitsshft  15197  setscom  15903  lubun  17123  grplmulf1o  17489  lmodfopne  18901  lidl1el  19218  frlmipval  20118  en2top  20789  cnpnei  21068  kgenidm  21350  ufileu  21723  fmfnfmlem4  21761  isngp4  22416  fsumcn  22673  evth  22758  mbfmulc2lem  23414  itg1addlem4  23466  dgreq0  24021  cxplt3  24446  cxple3  24447  basellem4  24810  axcontlem2  25845  umgr2edg  26101  nbumgrvtx  26242  umgrhashecclwwlk  26955  frgrncvvdeqlem9  27171  frgrwopreglem5ALT  27186  numclwwlk7lem  27247  grpoidinvlem3  27360  grpoideu  27363  grporcan  27372  3oalem2  28522  hmops  28879  adjadd  28952  mdslmd4i  29192  mdexchi  29194  mdsymlem1  29262  bnj607  30986  cvxsconn  31225  poseq  31750  sltsolem1  31826  nodenselem7  31840  tailfb  32372  poimirlem14  33423  mblfinlem4  33449  ismblfin  33450  ismtyres  33607  ghomco  33690  rngoisocnv  33780  1idl  33825  ps-2  34764  srhmsubc  42076  srhmsubcALTV  42094  aacllem  42547