Theorem ad2ant2lr 759

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

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrr 728	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 725	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  reusv2lem2  4618  mpteqb  5986  omxpenlem  7698  fineqvlem  7811  marypha1lem  7972  fin23lem26  8780  axdc3lem4  8908  mulcmpblnr  9520  ltsrpr  9526  sub4  9944  muladd  10078  ltleadd  10124  divdivdiv  10335  divadddiv  10349  ltmul12a  10488  lt2mul2div  10510  xlemul1a  11602  fzrev  11886  facndiv  12504  fsumconst  13899  fprodconst  14080  isprm5  14699  acsfn2  15617  ghmeql  16953  subgdmdprd  17715  lssvsubcl  18215  lssvacl  18225  lidlsubclOLD  18488  ocvin  19285  lindfmm  19433  scmatghm  19606  scmatmhm  19607  slesolinv  19753  slesolinvbi  19754  slesolex  19755  pm2mpf1lem  19866  pm2mpcoe1  19872  reftr  20577  alexsubALTlem2  21111  alexsubALTlem3  21112  blbas  21493  nmoco  21806  cncfmet  21988  cmetcaulem  22306  mbflimsup  22671  mbflimsupOLD  22672  ulmdvlem3  23405  ptolemy  23499  grpoideu  25985  ipblnfi  26545  htthlem  26618  hvaddsub4  26779  bralnfn  27649  hmops  27721  hmopm  27722  adjadd  27794  opsqrlem1  27841  atomli  28083  chirredlem2  28092  atcvat3i  28097  mdsymlem5  28108  cdj1i  28134  derangenlem  29942  elmrsubrn  30206  dfon2lem6  30482  poseq  30539  sltsolem1  30605  mblfinlem1  32021  prdsbnd  32169  heibor1lem  32185  hl2at  33014  congneg  35863  jm2.26  35901  stoweidlem34  37932  31wlkdlem6  39905  lindslinindsimp2  40528  ltsubaddb  40583  ltsubadd2b  40585  aacllem  40812