Theorem ad2ant2lr 784

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 753	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 750	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> 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:  reusv2lem2OLD  4870  mpteqb  6299  omxpenlem  8061  fineqvlem  8174  marypha1lem  8339  fin23lem26  9147  axdc3lem4  9275  mulcmpblnr  9892  ltsrpr  9898  sub4  10326  muladd  10462  ltleadd  10511  divdivdiv  10726  divadddiv  10740  ltmul12a  10879  lt2mul2div  10901  xlemul1a  12118  fzrev  12403  facndiv  13075  fsumconst  14522  fprodconst  14708  isprm5  15419  acsfn2  16324  ghmeql  17683  subgdmdprd  18433  lssvsubcl  18944  lssvacl  18954  ocvin  20018  lindfmm  20166  scmatghm  20339  scmatmhm  20340  slesolinv  20486  slesolinvbi  20487  slesolex  20488  pm2mpf1lem  20599  pm2mpcoe1  20605  reftr  21317  alexsubALTlem2  21852  alexsubALTlem3  21853  blbas  22235  nmoco  22541  cncfmet  22711  cmetcaulem  23086  mbflimsup  23433  ulmdvlem3  24156  ptolemy  24248  3wlkdlem6  27025  vdn0conngrumgrv2  27056  frgrncvvdeqlem8  27170  frgrwopreglem5ALT  27186  grpoideu  27363  ipblnfi  27711  htthlem  27774  hvaddsub4  27935  bralnfn  28807  hmops  28879  hmopm  28880  adjadd  28952  opsqrlem1  28999  atomli  29241  chirredlem2  29250  atcvat3i  29255  mdsymlem5  29266  cdj1i  29292  derangenlem  31153  elmrsubrn  31417  dfon2lem6  31693  poseq  31750  sltsolem1  31826  matunitlindflem1  33405  mblfinlem1  33446  prdsbnd  33592  heibor1lem  33608  hl2at  34691  congneg  37536  jm2.26  37569  stoweidlem34  40251  fmtnofac2lem  41480  lindslinindsimp2  42252  ltsubaddb  42304  ltsubadd2b  42306  aacllem  42547