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  5768  fiunsnnn  7138  addcomnqg  7696  addassnqg  7697  nqtri3or  7711  lt2addnq  7719  lt2mulnq  7720  enq0ref  7748  enq0tr  7749  nqnq0pi  7753  nqpnq0nq  7768  nqnq0a  7769  distrnq0  7774  addassnq0lemcl  7776  ltsrprg  8062  mulcomsrg  8072  mulasssrg  8073  distrsrg  8074  aptisr  8094  mulcnsr  8150  cnegex  8451  sub4  8518  muladd  8657  ltleadd  8720  divdivdivap  8987  divadddivap  9001  ltmul12a  9134  fzrev  10418  facndiv  11101  cncongr1  12800  ghmeql  13984  blbas  15298  cncfmet  15457  ptolemy  15689