Theorem ad2ant2lr 740

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 709	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 706	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  4482  mpteqb  5776  omxpenlem  7400  fineqvlem  7515  marypha1lem  7671  fin23lem26  8482  axdc3lem4  8610  mulcmpblnr  9229  ltsrpr  9232  sub4  9642  muladd  9765  ltleadd  9810  divdivdiv  10020  divadddiv  10034  ltmul12a  10173  lt2mul2div  10196  xlemul1a  11239  fzrev  11503  facndiv  12048  fsumconst  13240  isprm5  13781  acsfn2  14584  ghmeql  15749  subgdmdprd  16505  lssvsubcl  16947  lssvacl  16957  lidlsubcl  17220  ocvin  17941  lindfmm  18098  slesolinv  18328  slesolinvbi  18329  slesolex  18330  alexsubALTlem2  19462  alexsubALTlem3  19463  blbas  19847  nmoco  20158  cncfmet  20326  cmetcaulem  20641  mbflimsup  20986  ulmdvlem3  21752  ptolemy  21843  grpoideu  23519  ipblnfi  24079  htthlem  24142  hvaddsub4  24303  bralnfn  25175  hmops  25247  hmopm  25248  adjadd  25320  opsqrlem1  25367  atomli  25609  chirredlem2  25618  atcvat3i  25623  mdsymlem5  25634  cdj1i  25660  derangenlem  26907  fprodconst  27336  dfon2lem6  27448  poseq  27561  sltsolem1  27656  mblfinlem1  28272  prdsbnd  28536  heibor1lem  28552  congneg  29157  jm2.26  29196  stoweidlem34  29675  lindslinindsimp2  30706  hl2at  32622