Theorem ad2ant2lr 510

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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  mpteqb  5652  fiunsnnn  6942  addcomnqg  7448  addassnqg  7449  nqtri3or  7463  lt2addnq  7471  lt2mulnq  7472  enq0ref  7500  enq0tr  7501  nqnq0pi  7505  nqpnq0nq  7520  nqnq0a  7521  distrnq0  7526  addassnq0lemcl  7528  ltsrprg  7814  mulcomsrg  7824  mulasssrg  7825  distrsrg  7826  aptisr  7846  mulcnsr  7902  cnegex  8204  sub4  8271  muladd  8410  ltleadd  8473  divdivdivap  8740  divadddivap  8754  ltmul12a  8887  fzrev  10159  facndiv  10831  cncongr1  12271  ghmeql  13397  blbas  14669  cncfmet  14828  ptolemy  15060