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  5649  fiunsnnn  6939  addcomnqg  7443  addassnqg  7444  nqtri3or  7458  lt2addnq  7466  lt2mulnq  7467  enq0ref  7495  enq0tr  7496  nqnq0pi  7500  nqpnq0nq  7515  nqnq0a  7516  distrnq0  7521  addassnq0lemcl  7523  ltsrprg  7809  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  aptisr  7841  mulcnsr  7897  cnegex  8199  sub4  8266  muladd  8405  ltleadd  8467  divdivdivap  8734  divadddivap  8748  ltmul12a  8881  fzrev  10153  facndiv  10813  cncongr1  12244  ghmeql  13340  blbas  14612  cncfmet  14771  ptolemy  15000