Theorem ad2ant2lr 747

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 716	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 713	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

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:  reusv2lem2  4594  mpteqb  5889  omxpenlem  7514  fineqvlem  7630  marypha1lem  7786  fin23lem26  8597  axdc3lem4  8725  mulcmpblnr  9344  ltsrpr  9347  sub4  9757  muladd  9880  ltleadd  9925  divdivdiv  10135  divadddiv  10149  ltmul12a  10288  lt2mul2div  10311  xlemul1a  11354  fzrev  11622  facndiv  12167  fsumconst  13361  isprm5  13902  acsfn2  14705  ghmeql  15873  subgdmdprd  16638  lssvsubcl  17133  lssvacl  17143  lidlsubcl  17406  ocvin  18210  lindfmm  18367  slesolinv  18604  slesolinvbi  18605  slesolex  18606  alexsubALTlem2  19738  alexsubALTlem3  19739  blbas  20123  nmoco  20434  cncfmet  20602  cmetcaulem  20917  mbflimsup  21262  ulmdvlem3  21985  ptolemy  22076  grpoideu  23833  ipblnfi  24393  htthlem  24456  hvaddsub4  24617  bralnfn  25489  hmops  25561  hmopm  25562  adjadd  25634  opsqrlem1  25681  atomli  25923  chirredlem2  25932  atcvat3i  25937  mdsymlem5  25948  cdj1i  25974  derangenlem  27195  fprodconst  27625  dfon2lem6  27737  poseq  27850  sltsolem1  27945  mblfinlem1  28568  prdsbnd  28832  heibor1lem  28848  congneg  29452  jm2.26  29491  stoweidlem34  29969  lindslinindsimp2  31106  hl2at  33357