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  5670  fiunsnnn  6978  addcomnqg  7494  addassnqg  7495  nqtri3or  7509  lt2addnq  7517  lt2mulnq  7518  enq0ref  7546  enq0tr  7547  nqnq0pi  7551  nqpnq0nq  7566  nqnq0a  7567  distrnq0  7572  addassnq0lemcl  7574  ltsrprg  7860  mulcomsrg  7870  mulasssrg  7871  distrsrg  7872  aptisr  7892  mulcnsr  7948  cnegex  8250  sub4  8317  muladd  8456  ltleadd  8519  divdivdivap  8786  divadddivap  8800  ltmul12a  8933  fzrev  10206  facndiv  10884  cncongr1  12425  ghmeql  13603  blbas  14905  cncfmet  15064  ptolemy  15296