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  4489  mpteqb  5783  omxpenlem  7404  fineqvlem  7519  marypha1lem  7675  fin23lem26  8486  axdc3lem4  8614  mulcmpblnr  9233  ltsrpr  9236  sub4  9646  muladd  9769  ltleadd  9814  divdivdiv  10024  divadddiv  10038  ltmul12a  10177  lt2mul2div  10200  xlemul1a  11243  fzrev  11511  facndiv  12056  fsumconst  13249  isprm5  13790  acsfn2  14593  ghmeql  15760  subgdmdprd  16521  lssvsubcl  17005  lssvacl  17015  lidlsubcl  17278  ocvin  18079  lindfmm  18236  slesolinv  18466  slesolinvbi  18467  slesolex  18468  alexsubALTlem2  19600  alexsubALTlem3  19601  blbas  19985  nmoco  20296  cncfmet  20464  cmetcaulem  20779  mbflimsup  21124  ulmdvlem3  21847  ptolemy  21938  grpoideu  23664  ipblnfi  24224  htthlem  24287  hvaddsub4  24448  bralnfn  25320  hmops  25392  hmopm  25393  adjadd  25465  opsqrlem1  25512  atomli  25754  chirredlem2  25763  atcvat3i  25768  mdsymlem5  25779  cdj1i  25805  derangenlem  27028  fprodconst  27458  dfon2lem6  27570  poseq  27683  sltsolem1  27778  mblfinlem1  28399  prdsbnd  28663  heibor1lem  28679  congneg  29283  jm2.26  29322  stoweidlem34  29800  lindslinindsimp2  30928  hl2at  32942