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  4642  mpteqb  5955  omxpenlem  7608  fineqvlem  7724  marypha1lem  7882  fin23lem26  8694  axdc3lem4  8822  mulcmpblnr  9437  ltsrpr  9443  sub4  9853  muladd  9978  ltleadd  10024  divdivdiv  10234  divadddiv  10248  ltmul12a  10387  lt2mul2div  10410  xlemul1a  11469  fzrev  11731  facndiv  12321  fsumconst  13554  isprm5  14101  acsfn2  14907  ghmeql  16077  subgdmdprd  16864  lssvsubcl  17366  lssvacl  17376  lidlsubcl  17639  ocvin  18465  lindfmm  18622  scmatghm  18795  scmatmhm  18796  slesolinv  18942  slesolinvbi  18943  slesolex  18944  pm2mpf1lem  19055  pm2mpcoe1  19061  alexsubALTlem2  20276  alexsubALTlem3  20277  blbas  20661  nmoco  20972  cncfmet  21140  cmetcaulem  21455  mbflimsup  21801  ulmdvlem3  22524  ptolemy  22615  grpoideu  24737  ipblnfi  25297  htthlem  25360  hvaddsub4  25521  bralnfn  26393  hmops  26465  hmopm  26466  adjadd  26538  opsqrlem1  26585  atomli  26827  chirredlem2  26836  atcvat3i  26841  mdsymlem5  26852  cdj1i  26878  derangenlem  28105  fprodconst  28535  dfon2lem6  28647  poseq  28760  sltsolem1  28855  mblfinlem1  29479  prdsbnd  29743  heibor1lem  29759  congneg  30362  jm2.26  30401  stoweidlem34  31153  lindslinindsimp2  32012  hl2at  34076